finish is-fixed

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/smt/bv_solver.cpp

@@ -58,6 +58,15 @@ namespace bv {
         m_bb.set_flat(false);
     }
 
+    bool solver::is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) {
+        numeral n;
+        if (!get_fixed_value(v, n))
+            return false;
+        val = bv.mk_numeral(n, m_bits[v].size());
+        lits.append(m_bits[v]);
+        return true;
+    }
+
     void solver::fixed_var_eh(theory_var v1) {
         numeral val1, val2;
         VERIFY(get_fixed_value(v1, val1));

src/sat/smt/bv_solver.h

@@ -226,6 +226,7 @@ namespace bv {
         void get_bits(euf::enode* n, expr_ref_vector& r);
         void get_arg_bits(app* n, unsigned idx, expr_ref_vector& r);
         void fixed_var_eh(theory_var v);
+        bool is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) override;
         bool is_bv(theory_var v) const { return bv.is_bv(var2expr(v)); }
         void register_true_false_bit(theory_var v, unsigned i);
         void add_bit(theory_var v, sat::literal lit);

src/sat/smt/euf_solver.cpp

@@ -762,6 +762,25 @@ namespace euf {
     }
 
     bool solver::is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain) {
+        if (n->bool_var() != sat::null_bool_var) {
+            switch (s().value(n->bool_var())) {
+            case l_true:
+                val = m.mk_true();
+                explain.push_back(sat::literal(n->bool_var()));
+                return true;                
+            case l_false:
+                val = m.mk_false();
+                explain.push_back(~sat::literal(n->bool_var()));
+                return true;
+            default:
+                return false;
+            }
+        }
+        for (auto const& thv : enode_th_vars(n)) {
+            auto* th = m_id2solver.get(thv.get_id(), nullptr);
+            if (th && !th->is_fixed(thv.get_var(), val, explain))
+                return true;
+        }
         return false;
     }
 

src/sat/smt/sat_th.h

@@ -118,6 +118,8 @@ namespace euf {
 
         virtual bool enable_ackerman_axioms(euf::enode* n) const { return true; }
 
+        virtual bool is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) { return false; }
+
         virtual void relevant_eh(euf::enode* n) {}
 
         /**

src/smt/smt_context.cpp

@@ -2922,7 +2922,7 @@ namespace smt {
         while (l) {
             theory_id tid = l->get_id();
             auto* p = m_theories.get_plugin(tid);
-            if (p && p->is_fixed(l->get_var(), val, explain))
+            if (p && p->is_fixed_propagated(l->get_var(), val, explain))
                 return true;
             l = l->get_next();
         }

src/smt/smt_theory.h

@@ -620,7 +620,7 @@ namespace smt {
         /**
          * \brief theory plugin for fixed values.
          */
-        virtual bool is_fixed(theory_var v, expr_ref& val, literal_vector & explain) { return false; }
+        virtual bool is_fixed_propagated(theory_var v, expr_ref& val, literal_vector & explain) { return false; }
     };
     
 };

src/smt/theory_bv.cpp

@@ -519,7 +519,7 @@ namespace smt {
         }
     }
 
-    bool theory_bv::is_fixed(theory_var v, expr_ref& val, literal_vector& lits) {
+    bool theory_bv::is_fixed_propagated(theory_var v, expr_ref& val, literal_vector& lits) {
         numeral r;
         enode* n = get_enode(v);
         if (!get_fixed_value(v, r))

src/smt/theory_bv.h

@@ -282,7 +282,7 @@ namespace smt {
         void collect_statistics(::statistics & st) const override;
 
         bool get_fixed_value(app* x, numeral & result) const;
-        bool is_fixed(theory_var v, expr_ref& val, literal_vector& explain) override;
+        bool is_fixed_propagated(theory_var v, expr_ref& val, literal_vector& explain) override;
 
         bool check_assignment(theory_var v);
         bool check_invariant();