Prevent double-definitions of propositions (#488)

* prevent double-definitions

* add cvc5 testing

Author: UnsignedByte

crates/filament/src/ir_passes/discharge.rs

@@ -9,7 +9,7 @@ use fil_ast as ast;
 use fil_ir::{self as ir, Ctx, DisplayCtx};
 use fil_utils::GlobalPositionTable;
 use itertools::Itertools;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use std::{fs, iter};
 use term::termcolor::{ColorChoice, StandardStream};
 
@@ -608,6 +608,9 @@ impl Visitor for Discharge {
         }
 
         let bs = self.sol.bool_sort();
+
+        let mut interned_props = HashSet::new();
+
         // Declare all expressions
         for (idx, expr) in data
             .comp
@@ -622,6 +625,9 @@ impl Visitor for Discharge {
                 .map(|i| (i, data.comp.get(i)));
 
             for (pidx, prop) in relevant_props {
+                // Save the proposition in the interned_props set
+                interned_props.insert(pidx);
+
                 let assign = self.prop_to_sexp(prop);
                 let sexp = self
                     .sol
@@ -675,6 +681,8 @@ impl Visitor for Discharge {
             .props()
             .iter()
             .filter(|(idx, _)| idx.valid(&data.comp))
+            // Filter out propositions that are already defined in expressions
+            .filter(|(idx, _)| !interned_props.contains(idx))
         {
             // Define assertion equating the proposition to its assignment
             let assign = self.prop_to_sexp(prop);

runt.toml

@@ -2,10 +2,18 @@ ver = "0.4.1"
 
 
 [[tests]]
-name = "check"
+name = "check-z3"
 paths = ["tests/check/*.fil", "primitives/*.fil"]
 cmd = """
-./target/debug/filament {} --check
+./target/debug/filament {} --check --solver z3
+"""
+expect_dir = "tests/check/"
+
+[[tests]]
+name = "check-cvc5"
+paths = ["tests/check/*.fil", "primitives/*.fil"]
+cmd = """
+./target/debug/filament {} --check --solver cvc5
 """
 expect_dir = "tests/check/"