Parse existentials in annotations

.github/workflows/ci.yml

@@ -24,9 +24,33 @@ jobs:
     runs-on: ubuntu-latest
     permissions:
       contents: read
+    env:
+      COAR_IMAGE: ghcr.io/hiroshi-unno/coar@sha256:73144ed27a02b163d1a71b41b58f3b5414f12e91326015600cfdca64ff19f011
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/actions/setup-z3
+      - name: Setup thrust-pcsat-wrapper
+        run: |
+          docker pull "$COAR_IMAGE"
+
+          cat <<"EOF" > thrust-pcsat-wrapper
+          #!/bin/bash
+
+          smt2=$(mktemp -p . --suffix .smt2)
+          trap "rm -f $smt2" EXIT
+          cp "$1" "$smt2"
+          out=$(
+            docker run --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \
+              main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2"
+          )
+          exit_code=$?
+          echo "${out%,*}"
+          exit "$exit_code"
+          EOF
+          chmod +x thrust-pcsat-wrapper
+
+          mkdir -p ~/.local/bin
+          mv thrust-pcsat-wrapper ~/.local/bin/thrust-pcsat-wrapper
       - run: rustup show
       - uses: Swatinem/rust-cache@v2
       - run: cargo test

src/annot.rs

@@ -12,6 +12,7 @@ use rustc_ast::token::{BinOpToken, Delimiter, LitKind, Token, TokenKind};
 use rustc_ast::tokenstream::{RefTokenTreeCursor, Spacing, TokenStream, TokenTree};
 use rustc_index::IndexVec;
 use rustc_span::symbol::Ident;
+use std::collections::HashMap;
 
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
@@ -185,6 +186,7 @@ impl<T> FormulaOrTerm<T> {
 struct Parser<'a, T> {
     resolver: T,
     cursor: RefTokenTreeCursor<'a>,
+    formula_existentials: HashMap<String, chc::Sort>,
 }
 
 impl<'a, T> Parser<'a, T>
@@ -232,6 +234,15 @@ where
         }
     }
 
+    fn expect_next_ident(&mut self) -> Result<Ident> {
+        let t = self.next_token("ident")?;
+        if let Some((ident, _)) = t.ident() {
+            Ok(ident)
+        } else {
+            Err(ParseAttrError::unexpected_token("ident", t.clone()))
+        }
+    }
+
     fn consume(&mut self) {
         self.cursor.next().unwrap();
     }
@@ -296,6 +307,7 @@ where
                 let mut parser = Parser {
                     resolver: self.boxed_resolver(),
                     cursor: s.trees(),
+                    formula_existentials: self.formula_existentials.clone(),
                 };
                 let formula_or_term = parser.parse_formula_or_term_or_tuple()?;
                 parser.end_of_input()?;
@@ -305,9 +317,17 @@ where
         };
 
         let formula_or_term = if let Some((ident, _)) = t.ident() {
-            match ident.as_str() {
-                "true" => FormulaOrTerm::Formula(chc::Formula::top()),
-                "false" => FormulaOrTerm::Formula(chc::Formula::bottom()),
+            match (
+                ident.as_str(),
+                self.formula_existentials.get(ident.name.as_str()),
+            ) {
+                ("true", _) => FormulaOrTerm::Formula(chc::Formula::top()),
+                ("false", _) => FormulaOrTerm::Formula(chc::Formula::bottom()),
+                (_, Some(sort)) => {
+                    let var =
+                        chc::Term::FormulaExistentialVar(sort.clone(), ident.name.to_string());
+                    FormulaOrTerm::Term(var, sort.clone())
+                }
                 _ => {
                     let (v, sort) = self.resolve(ident)?;
                     FormulaOrTerm::Term(chc::Term::var(v), sort)
@@ -575,8 +595,94 @@ where
         Ok(formula_or_term)
     }
 
+    fn parse_exists(&mut self) -> Result<FormulaOrTerm<T::Output>> {
+        match self.look_ahead_token(0) {
+            Some(Token {
+                kind: TokenKind::Ident(sym, _),
+                ..
+            }) if sym.as_str() == "exists" => {
+                self.consume();
+                let mut vars = Vec::new();
+                loop {
+                    let ident = self.expect_next_ident()?;
+                    self.expect_next_token(TokenKind::Colon, ":")?;
+                    let sort = self.parse_sort()?;
+                    vars.push((ident.name.to_string(), sort));
+                    match self.next_token(". or ,")? {
+                        Token {
+                            kind: TokenKind::Comma,
+                            ..
+                        } => {}
+                        Token {
+                            kind: TokenKind::Dot,
+                            ..
+                        } => break,
+                        t => return Err(ParseAttrError::unexpected_token(". or ,", t.clone())),
+                    }
+                }
+                self.formula_existentials.extend(vars.iter().cloned());
+                let formula = self
+                    .parse_formula_or_term()?
+                    .into_formula()
+                    .ok_or_else(|| ParseAttrError::unexpected_term("in exists formula"))?;
+                for (name, _) in &vars {
+                    self.formula_existentials.remove(name);
+                }
+                Ok(FormulaOrTerm::Formula(chc::Formula::exists(vars, formula)))
+            }
+            _ => self.parse_binop_5(),
+        }
+    }
+
     fn parse_formula_or_term(&mut self) -> Result<FormulaOrTerm<T::Output>> {
-        self.parse_binop_5()
+        self.parse_exists()
+    }
+
+    fn parse_sort(&mut self) -> Result<chc::Sort> {
+        let tt = self.next_token_tree("sort")?.clone();
+        match tt {
+            TokenTree::Token(
+                Token {
+                    kind: TokenKind::Ident(sym, _),
+                    ..
+                },
+                _,
+            ) => {
+                let sort = match sym.as_str() {
+                    "bool" => chc::Sort::bool(),
+                    "int" => chc::Sort::int(),
+                    "string" => unimplemented!(),
+                    "null" => chc::Sort::null(),
+                    "fn" => unimplemented!(),
+                    _ => unimplemented!(),
+                };
+                Ok(sort)
+            }
+            TokenTree::Delimited(_, _, Delimiter::Parenthesis, ts) => {
+                let mut parser = Parser {
+                    resolver: self.boxed_resolver(),
+                    cursor: ts.trees(),
+                    formula_existentials: self.formula_existentials.clone(),
+                };
+                let mut sorts = Vec::new();
+                loop {
+                    sorts.push(parser.parse_sort()?);
+                    match parser.look_ahead_token(0) {
+                        Some(Token {
+                            kind: TokenKind::Comma,
+                            ..
+                        }) => {
+                            parser.consume();
+                        }
+                        None => break,
+                        Some(t) => return Err(ParseAttrError::unexpected_token(",", t.clone())),
+                    }
+                }
+                parser.end_of_input()?;
+                Ok(chc::Sort::tuple(sorts))
+            }
+            t => Err(ParseAttrError::unexpected_token_tree("sort", t.clone())),
+        }
     }
 
     fn parse_ty(&mut self) -> Result<rty::Type<T::Output>> {
@@ -662,6 +768,7 @@ where
                 let mut parser = Parser {
                     resolver: self.boxed_resolver(),
                     cursor: ts.trees(),
+                    formula_existentials: self.formula_existentials.clone(),
                 };
                 let mut rtys = Vec::new();
                 loop {
@@ -697,6 +804,7 @@ where
         let mut parser = Parser {
             resolver: self.boxed_resolver(),
             cursor: ts.trees(),
+            formula_existentials: self.formula_existentials.clone(),
         };
         let self_ident = if matches!(
             parser.look_ahead_token(1),
@@ -720,6 +828,7 @@ where
         let mut parser = Parser {
             resolver: RefinementResolver::new(self.boxed_resolver()),
             cursor: parser.cursor,
+            formula_existentials: self.formula_existentials.clone(),
         };
         if let Some(self_ident) = self_ident {
             parser.resolver.set_self(self_ident, ty.to_sort());
@@ -859,6 +968,7 @@ where
         let mut parser = Parser {
             resolver: &self.resolver,
             cursor: ts.trees(),
+            formula_existentials: Default::default(),
         };
         let rty = parser.parse_rty()?;
         parser.end_of_input()?;
@@ -869,6 +979,7 @@ where
         let mut parser = Parser {
             resolver: &self.resolver,
             cursor: ts.trees(),
+            formula_existentials: Default::default(),
         };
         let formula = parser.parse_annot_formula()?;
         parser.end_of_input()?;

src/chc.rs

@@ -406,6 +406,8 @@ pub enum Term<V = TermVarIdx> {
     TupleProj(Box<Term<V>>, usize),
     DatatypeCtor(DatatypeSort, DatatypeSymbol, Vec<Term<V>>),
     DatatypeDiscr(DatatypeSymbol, Box<Term<V>>),
+    /// Used in [`Formula`] to represent existentially quantified variables appearing in annotations.
+    FormulaExistentialVar(Sort, String),
 }
 
 impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Term<V>
@@ -475,6 +477,7 @@ where
             Term::DatatypeDiscr(_, t) => allocator
                 .text("discriminant")
                 .append(t.pretty(allocator).parens()),
+            Term::FormulaExistentialVar(_, name) => allocator.text(name.clone()),
         }
     }
 }
@@ -521,6 +524,7 @@ impl<V> Term<V> {
                 args.into_iter().map(|t| t.subst_var(&mut f)).collect(),
             ),
             Term::DatatypeDiscr(d_sym, t) => Term::DatatypeDiscr(d_sym, Box::new(t.subst_var(f))),
+            Term::FormulaExistentialVar(sort, name) => Term::FormulaExistentialVar(sort, name),
         }
     }
 
@@ -562,15 +566,18 @@ impl<V> Term<V> {
             Term::TupleProj(t, i) => t.sort(var_sort).tuple_elem(*i),
             Term::DatatypeCtor(sort, _, _) => sort.clone().into(),
             Term::DatatypeDiscr(_, _) => Sort::int(),
+            Term::FormulaExistentialVar(sort, _) => sort.clone(),
         }
     }
 
     fn fv_impl(&self) -> Box<dyn Iterator<Item = &V> + '_> {
         match self {
             Term::Var(v) => Box::new(std::iter::once(v)),
-            Term::Null | Term::Bool(_) | Term::Int(_) | Term::String(_) => {
-                Box::new(std::iter::empty())
-            }
+            Term::Null
+            | Term::Bool(_)
+            | Term::Int(_)
+            | Term::String(_)
+            | Term::FormulaExistentialVar { .. } => Box::new(std::iter::empty()),
             Term::Box(t) => t.fv_impl(),
             Term::Mut(t1, t2) => Box::new(t1.fv_impl().chain(t2.fv_impl())),
             Term::BoxCurrent(t) => t.fv_impl(),
@@ -1083,6 +1090,7 @@ pub enum Formula<V = TermVarIdx> {
     Not(Box<Formula<V>>),
     And(Vec<Formula<V>>),
     Or(Vec<Formula<V>>),
+    Exists(Vec<(String, Sort)>, Box<Formula<V>>),
 }
 
 impl<V> Default for Formula<V> {
@@ -1124,6 +1132,25 @@ where
                 );
                 inner.group()
             }
+            Formula::Exists(vars, fo) => {
+                let vars = allocator.intersperse(
+                    vars.iter().map(|(name, sort)| {
+                        allocator
+                            .text(name.clone())
+                            .append(allocator.text(":"))
+                            .append(allocator.text(" "))
+                            .append(sort.pretty(allocator))
+                    }),
+                    allocator.text(", ").append(allocator.line()),
+                );
+                allocator
+                    .text("∃")
+                    .append(vars)
+                    .append(allocator.text("."))
+                    .append(allocator.line())
+                    .append(fo.pretty(allocator).nest(2))
+                    .group()
+            }
         }
     }
 }
@@ -1139,7 +1166,9 @@ impl<V> Formula<V> {
         D::Doc: Clone,
     {
         match self {
-            Formula::And(_) | Formula::Or(_) => self.pretty(allocator).parens(),
+            Formula::And(_) | Formula::Or(_) | Formula::Exists { .. } => {
+                self.pretty(allocator).parens()
+            }
             _ => self.pretty(allocator),
         }
     }
@@ -1158,6 +1187,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => fo.is_bottom(),
             Formula::And(fs) => fs.iter().all(Formula::is_top),
             Formula::Or(fs) => fs.iter().any(Formula::is_top),
+            Formula::Exists(_, fo) => fo.is_top(),
         }
     }
 
@@ -1167,6 +1197,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => fo.is_top(),
             Formula::And(fs) => fs.iter().any(Formula::is_bottom),
             Formula::Or(fs) => fs.iter().all(Formula::is_bottom),
+            Formula::Exists(_, fo) => fo.is_bottom(),
         }
     }
 
@@ -1197,6 +1228,10 @@ impl<V> Formula<V> {
         }
     }
 
+    pub fn exists(vars: Vec<(String, Sort)>, body: Self) -> Self {
+        Formula::Exists(vars, Box::new(body))
+    }
+
     pub fn subst_var<F, W>(self, f: F) -> Formula<W>
     where
         F: FnMut(V) -> Term<W>,
@@ -1210,6 +1245,7 @@ impl<V> Formula<V> {
                 Formula::And(fs.into_iter().map(|fo| fo.subst_var(&mut f)).collect())
             }
             Formula::Or(fs) => Formula::Or(fs.into_iter().map(|fo| fo.subst_var(&mut f)).collect()),
+            Formula::Exists(vars, fo) => Formula::Exists(vars, Box::new(fo.subst_var(f))),
         }
     }
 
@@ -1224,6 +1260,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => Formula::Not(Box::new(fo.map_var(&mut f))),
             Formula::And(fs) => Formula::And(fs.into_iter().map(|fo| fo.map_var(&mut f)).collect()),
             Formula::Or(fs) => Formula::Or(fs.into_iter().map(|fo| fo.map_var(&mut f)).collect()),
+            Formula::Exists(vars, fo) => Formula::Exists(vars, Box::new(fo.map_var(f))),
         }
     }
 
@@ -1237,6 +1274,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => Box::new(fo.fv()),
             Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::fv)),
             Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::fv)),
+            Formula::Exists(_, fo) => Box::new(fo.fv()),
         }
     }
 
@@ -1250,6 +1288,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => Box::new(fo.iter_atoms()),
             Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),
             Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),
+            Formula::Exists(_, fo) => Box::new(fo.iter_atoms()),
         }
     }
 
@@ -1291,6 +1330,9 @@ impl<V> Formula<V> {
                     *self = fs.pop().unwrap();
                 }
             }
+            Formula::Exists(_, fo) => {
+                fo.simplify();
+            }
         }
     }
 }

src/chc/format_context.rs

@@ -57,6 +57,7 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet<chc::Sor
             }
         }
         chc::Term::DatatypeDiscr(_, t) => term_sorts(clause, t, sorts),
+        chc::Term::FormulaExistentialVar(_, _) => {}
     }
 }