break things because exists binding logic is wrong

src/ir/comp.rs

@@ -58,9 +58,6 @@ pub struct Component {
     /// Facts defined in the component signature
     pub facts: Vec<Fact>,
 
-    /// Existentially quantified parameters and their binding
-    pub exists_params: Vec<(ParamIdx, Option<ExprIdx>)>,
-
     /// Commands in the component
     pub cmds: Vec<Command>,
 

src/ir/control.rs

@@ -21,6 +21,8 @@ pub enum Command {
     If(If),
     /// An `assume` or `assert` fact
     Fact(Fact),
+    /// An `exists` binding
+    Exists(Exists),
 }
 impl Command {
     pub fn is_loop(&self) -> bool {
@@ -66,6 +68,11 @@ impl From<Fact> for Command {
         Command::Fact(fact)
     }
 }
+impl From<Exists> for Command {
+    fn from(exists: Exists) -> Self {
+        Command::Exists(exists)
+    }
+}
 
 #[derive(Clone, PartialEq, Eq)]
 /// An instantiated component
@@ -183,3 +190,11 @@ impl EventBind {
         }
     }
 }
+
+#[derive(Clone, PartialEq, Eq)]
+pub struct Exists {
+    /// The existentially quantified parameter
+    pub param: ParamIdx,
+    /// The binding for the parameter
+    pub expr: ExprIdx,
+}

src/ir/fact.rs

@@ -14,7 +14,7 @@ impl fmt::Display for Cmp {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         let op = match self {
             Cmp::Gt => ">",
-            Cmp::Eq => "=",
+            Cmp::Eq => "==",
             Cmp::Gte => ">=",
         };
         write!(f, "{}", op)

src/ir/from_ast/astconv.rs

@@ -3,8 +3,8 @@ use super::build_ctx::{OwnedParam, OwnedPort};
 use super::{BuildCtx, Sig, SigMap};
 use crate::diagnostics;
 use crate::ir::{
-    AddCtx, Cmp, Ctx, EventIdx, ExprIdx, InterfaceSrc, MutCtx, ParamIdx,
-    PortIdx, PropIdx, TimeIdx,
+    AddCtx, Cmp, Ctx, DisplayCtx, EventIdx, ExprIdx, InterfaceSrc, MutCtx,
+    ParamIdx, PortIdx, PropIdx, TimeIdx,
 };
 use crate::utils::{GPosIdx, Idx};
 use crate::{ast, ir};
@@ -545,9 +545,7 @@ impl<'prog> BuildCtx<'prog> {
                     self.add_let_param(param.copy(), e);
                 }
                 ast::SigBind::Exists { param, cons } => {
-                    let p_idx =
-                        self.param(param.clone(), ir::ParamOwner::Exists);
-                    self.add_exists_param(p_idx);
+                    self.param(param.clone(), ir::ParamOwner::Exists);
                     // Constraints on existentially quantified parameters
                     for pc in cons {
                         let info = self.comp().add(ir::Info::assert(
@@ -819,8 +817,15 @@ impl<'prog> BuildCtx<'prog> {
             ast::Command::Instance(inst) => self.instance(inst)?,
             ast::Command::Exists(ast::Exists { param, bind }) => {
                 let expr = self.expr(bind.inner().clone())?;
-                self.set_exists_bind(param, expr)?;
-                vec![]
+                let owner = OwnedParam::Local(param.copy());
+                let param_expr = self.get_param(&owner, param.pos())?;
+                let Some(param) = param_expr.as_param(self.comp()) else {
+                    unreachable!(
+                        "Existing LHS is an expression: {}",
+                        self.comp().display(param_expr)
+                    )
+                };
+                vec![ir::Exists { param, expr }.into()]
             }
             ast::Command::Fact(ast::Fact { cons, checked }) => {
                 let reason = self.comp().add(

src/ir/from_ast/build_ctx.rs

@@ -218,56 +218,6 @@ impl<'prog> BuildCtx<'prog> {
         self.param_map.insert(OwnedParam::Local(id), expr);
     }
 
-    /// Mark a parameter as existentially quantified.
-    pub fn add_exists_param(&mut self, param: ir::ParamIdx) {
-        self.comp.exists_params.push((param, None));
-    }
-
-    /// Provide the binding for an existentially quantified parameter.
-    pub fn set_exists_bind(
-        &mut self,
-        param: ast::Loc<Id>,
-        expr: ir::ExprIdx,
-    ) -> BuildRes<()> {
-        let p_idx = self
-            .get_param(&OwnedParam::local(param.copy()), param.pos())?
-            .as_param(&self.comp)
-            .unwrap();
-        let diag = &mut self.diag;
-
-        if let Some((_, bind)) = self
-            .comp
-            .exists_params
-            .iter_mut()
-            .find(|(p, _)| *p == p_idx)
-        {
-            // If there is already a binding, then we have a problem
-            if bind.is_some() {
-                let msg = format!(
-                    "existential parameter `{param}' already has a binding",
-                    param = param
-                );
-                let err = Error::malformed(msg.clone())
-                    .add_note(diag.add_info(msg, param.pos()));
-                diag.add_error(err);
-                return Err(std::mem::take(diag));
-            }
-            *bind = Some(expr);
-            Ok(())
-        } else {
-            let msg = format!(
-                "parameter `{param}' is not existentially quantified",
-                param = param
-            );
-            let err = Error::malformed(msg).add_note(diag.add_info(
-                "parameter is not existentially quantified",
-                param.pos(),
-            ));
-            diag.add_error(err);
-            Err(std::mem::take(diag))
-        }
-    }
-
     pub fn get_param(
         &mut self,
         param: &OwnedParam,

src/ir/mod.rs

@@ -17,7 +17,9 @@ mod validate;
 
 pub use comp::Component;
 pub use context::Context;
-pub use control::{Command, Connect, EventBind, If, Instance, Invoke, Loop};
+pub use control::{
+    Command, Connect, EventBind, Exists, If, Instance, Invoke, Loop,
+};
 pub use ctx::{AddCtx, Ctx, MutCtx};
 pub use expr::Expr;
 pub use fact::{Cmp, CmpOp, Fact, Prop};

src/ir/printer/comp.rs

@@ -75,13 +75,18 @@ impl<'a> Printer<'a> {
                 write!(f, "{:indent$}}}", "")
             }
             ir::Command::If(c) => {
-                writeln!(f, "{:indent$}if {} {{", "", c.cond)?;
+                writeln!(
+                    f,
+                    "{:indent$}if {} {{",
+                    "",
+                    self.ctx.display(c.cond)
+                )?;
                 self.commands(&c.then, indent + 2, f)?;
-                writeln!(f, "{:indent$}}}", "")?;
+                write!(f, "{:indent$}}}", "")?;
                 if !c.alt.is_empty() {
-                    writeln!(f, "{:indent$}else {{", "")?;
+                    writeln!(f, " else {{")?;
                     self.commands(&c.alt, indent + 2, f)?;
-                    writeln!(f, "{:indent$}}}", "")?;
+                    write!(f, "{:indent$}}}", "")?;
                 }
                 Ok(())
             }
@@ -102,6 +107,15 @@ impl<'a> Printer<'a> {
                     )
                 }
             }
+            ir::Command::Exists(ir::Exists { param, expr }) => {
+                write!(
+                    f,
+                    "{:indent$}exists {} = {};",
+                    "",
+                    self.ctx.display(*param),
+                    self.ctx.display(*expr)
+                )
+            }
         }
     }
 

src/ir/utils/traversal.rs

@@ -103,7 +103,8 @@ impl Traversal {
             ir::Command::Connect(_)
             | ir::Command::BundleDef(_)
             | ir::Command::Invoke(_)
-            | ir::Command::Fact(_) => (),
+            | ir::Command::Fact(_)
+            | ir::Command::Exists(_) => (),
         }
     }
 }

src/ir/validate.rs

@@ -210,12 +210,12 @@ impl<'a> Validate<'a> {
     /// (1) It is defined in the component
     /// (2) Its owner is defined in the component
     /// (3) Its owner points to it?
-    fn param(&self, pidx: ir::ParamIdx) {
+    fn param(&self, pidx: ir::ParamIdx) -> &ir::Param {
         // check (1) - this will panic if param not defined
-        let ir::Param { owner, .. } = &self.comp.get(pidx);
+        let param = &self.comp.get(pidx);
 
         // check (2) and (3)
-        match owner {
+        match &param.owner {
             ir::ParamOwner::Sig
             | ir::ParamOwner::Exists
             | ir::ParamOwner::Loop => { /* Nothing to check */ }
@@ -232,6 +232,8 @@ impl<'a> Validate<'a> {
                 }
             }
         }
+
+        param
     }
 
     /// An invoke is valid if:
@@ -314,27 +316,14 @@ impl<'a> Validate<'a> {
     /// (1) The structures that it contains are valid
     fn command(&self, cmd: &ir::Command) {
         match cmd {
-            ir::Command::Instance(iidx) => {
-                self.instance(*iidx);
-            }
-            ir::Command::Invoke(iidx) => {
-                self.invoke(*iidx);
-            }
-            ir::Command::Connect(con) => {
-                self.connect(con);
-            }
-            ir::Command::ForLoop(lp) => {
-                self.forloop(lp);
-            }
-            ir::Command::If(cond) => {
-                self.if_stmt(cond);
-            }
-            ir::Command::Fact(fact) => {
-                self.fact(fact);
-            }
-            ir::Command::BundleDef(b) => {
-                self.bundle_def(*b);
-            }
+            ir::Command::Instance(iidx) => self.instance(*iidx),
+            ir::Command::Invoke(iidx) => self.invoke(*iidx),
+            ir::Command::Connect(con) => self.connect(con),
+            ir::Command::ForLoop(lp) => self.forloop(lp),
+            ir::Command::If(cond) => self.if_stmt(cond),
+            ir::Command::Fact(fact) => self.fact(fact),
+            ir::Command::BundleDef(b) => self.bundle_def(*b),
+            ir::Command::Exists(e) => self.exists(e),
         }
     }
 
@@ -439,4 +428,17 @@ impl<'a> Validate<'a> {
         let ir::Fact { prop, .. } = *fact;
         self.prop(prop);
     }
+
+    fn exists(&self, exists: &ir::Exists) {
+        let ir::Exists { param: p_idx, expr } = exists;
+        let param = self.param(*p_idx);
+        if !matches!(param.owner, ir::ParamOwner::Exists) {
+            self.comp.internal_error(format!(
+                "{} mentioned in existential binding but owned by {}",
+                self.comp.display(*p_idx),
+                param.owner
+            ))
+        }
+        self.expr(*expr);
+    }
 }

src/ir_passes/discharge.rs

@@ -22,7 +22,7 @@ impl Assign {
             .iter()
             .filter_map(|(k, v)| {
                 // Attempt to parse value as a number
-                match v.parse::<u64>() {
+                match v.parse::<i64>() {
                     Ok(v) if v == 0 => None,
                     _ => Some(format!("{} = {v}", ctx.display(*k))),
                 }
@@ -133,12 +133,14 @@ impl Construct for Discharge {
 }
 
 impl Discharge {
-    fn fmt_param(param: ir::ParamIdx) -> String {
-        format!("param{}", param.get())
+    fn fmt_param(param: ir::ParamIdx, ctx: &ir::Component) -> String {
+        format!("|{}@param{}|", ctx.display(param), param.get())
+        // format!("param{}", param.get())
     }
 
-    fn fmt_event(event: ir::EventIdx) -> String {
-        format!("event{}", event.get())
+    fn fmt_event(event: ir::EventIdx, ctx: &ir::Component) -> String {
+        format!("|{}@event{}|", ctx.display(event), event.get())
+        // format!("event{}", event.get())
     }
 
     fn fmt_expr(expr: ir::ExprIdx) -> String {
@@ -191,19 +193,30 @@ impl Discharge {
             .unique()
             .map(|p| {
                 let s = self.param_map[*p];
+                log::debug!("{} -> {}", self.sol.display(s), p);
                 rev_map.insert(s, *p);
                 s
             })
             .collect_vec();
+        let num_vars = sexps.len();
+
+        let model = self.sol.get_value(sexps).unwrap();
+        assert!(model.len() == num_vars,
+            "{num_vars} relevant variables but the model contains assignments for {} variables",
+            model.len()
+        );
 
         Assign(
-            self.sol
-                .get_value(sexps)
-                .unwrap()
+            model
                 .into_iter()
-                .map(|(p, v)| {
-                    let p = rev_map[&p];
-                    (p, self.sol.display(v).to_string())
+                .flat_map(|(p, v)| {
+                    let Some(&p) = rev_map.get(&p) else {
+                        unreachable!(
+                            "missing binding for sexp {}",
+                            self.sol.display(p)
+                        );
+                    };
+                    Some((p, self.sol.display(v).to_string()))
                 })
                 .collect_vec(),
         )
@@ -225,7 +238,6 @@ impl Discharge {
                 ctx.display(prop.consequent(ctx));
                 100
             );
-            self.sol.assert(self.sol.not(actlit)).unwrap();
             let out = match res {
                 smt::Response::Sat => {
                     if self.show_models {
@@ -239,6 +251,8 @@ impl Discharge {
                 smt::Response::Unsat => None,
                 smt::Response::Unknown => panic!("Solver returned unknown"),
             };
+            // Deassert the actlit after the `get-model` call.
+            self.sol.assert(self.sol.not(actlit)).unwrap();
             self.checked.insert(prop, out);
         }
         if let Some(assign) = &self.checked[&prop] {
@@ -359,12 +373,13 @@ impl Visitor for Discharge {
     }
 
     fn start(&mut self, data: &mut VisitorData) -> Action {
+        let comp = &data.comp;
         // Declare all parameters
         let int = self.sol.int_sort();
         for (idx, _) in data.comp.params().iter() {
             let sexp = self
                 .sol
-                .declare_fun(Self::fmt_param(idx), vec![], int)
+                .declare_fun(Self::fmt_param(idx, comp), vec![], int)
                 .unwrap();
             self.param_map.push(idx, sexp);
         }
@@ -373,7 +388,7 @@ impl Visitor for Discharge {
         for (idx, _) in data.comp.events().iter() {
             let sexp = self
                 .sol
-                .declare_fun(Self::fmt_event(idx), vec![], int)
+                .declare_fun(Self::fmt_event(idx, comp), vec![], int)
                 .unwrap();
             self.ev_map.push(idx, sexp);
         }