misc

src/ast/arith_decl_plugin.cpp

@@ -595,6 +595,7 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
     op_names.push_back(builtin_name("abs", OP_ABS));
     if (logic == symbol::null || logic == symbol("ALL")) {
         op_names.push_back(builtin_name("^", OP_POWER));
+        op_names.push_back(builtin_name("^0", OP_POWER0));
         op_names.push_back(builtin_name("sin", OP_SIN));
         op_names.push_back(builtin_name("cos", OP_COS));
         op_names.push_back(builtin_name("tan", OP_TAN));

src/ast/arith_decl_plugin.h

@@ -294,6 +294,7 @@ class arith_recognizers {
     bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); }
     bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); }
     bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); }
+    bool is_power0(expr const * n) const { return is_app_of(n, m_afid, OP_POWER0); }
 
     bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
     bool is_int(expr const * n) const { return is_int(get_sort(n)); }

src/sat/smt/arith_axioms.cpp

@@ -49,6 +49,14 @@ namespace arith {
         }
     }
 
+    // t = n^0
+    void solver::mk_power0_axioms(app* t, app* n) {
+        expr_ref p0(a.mk_power0(n, t->get_arg(1)), m);
+        literal eq = eq_internalize(n, a.mk_numeral(rational(0), a.is_int(n)));
+        add_clause(~eq, eq_internalize(t, p0));
+        add_clause(eq, eq_internalize(t, a.mk_numeral(rational(1), a.is_int(t))));
+    }
+
     // is_int(x) <=> to_real(to_int(x)) = x
     void solver::mk_is_int_axiom(expr* n) {
         expr* x = nullptr;

src/sat/smt/arith_internalize.cpp

@@ -265,7 +265,7 @@ namespace arith {
                     st.to_ensure_var().push_back(n1);
                     st.to_ensure_var().push_back(n2);
                 }
-                else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n)) {
+                else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) {
                     found_unsupported(n);
                 }
                 else {
@@ -437,12 +437,18 @@ namespace arith {
             return v;
         theory_var w = mk_evar(n);
         internalize_term(n);
-        svector<lpvar> vars;
-        for (unsigned i = 0; i < p; ++i)
-            vars.push_back(register_theory_var_in_lar_solver(w));
-        ensure_nla();
-        m_solver->register_existing_terms();
-        m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
+
+        if (p == 0) {
+            mk_power0_axioms(t, n);
+        }
+        else {
+            svector<lpvar> vars;
+            for (unsigned i = 0; i < p; ++i)
+                vars.push_back(register_theory_var_in_lar_solver(w));
+            ensure_nla();
+            m_solver->register_existing_terms();
+            m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
+        }
         return v;
     }
 
@@ -566,6 +572,7 @@ namespace arith {
                 for (expr* arg : *to_app(e))
                     args.push_back(e_internalize(arg));
             n = ctx.mk_enode(e, args.size(), args.c_ptr());
+            ctx.attach_node(n);
         }
         return n;
     }

src/sat/smt/arith_solver.cpp

@@ -1127,7 +1127,7 @@ namespace arith {
             set_evidence(ev.ci(), m_core, m_eqs);
         DEBUG_CODE(
             if (is_conflict) {
-                for (literal c : m_core) VERIFY(s().value(c) == l_false);
+                for (literal c : m_core) VERIFY(s().value(c) == l_true);
                 for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());
             });
         for (auto const& eq : m_eqs)

src/sat/smt/arith_solver.h

@@ -267,6 +267,7 @@ namespace arith {
         void mk_rem_axiom(expr* dividend, expr* divisor);
         void mk_bound_axioms(api_bound& b);
         void mk_bound_axiom(api_bound& b1, api_bound& b2);
+        void mk_power0_axioms(app* t, app* n);
         void flush_bound_axioms();
 
         // bounds

src/sat/smt/euf_internalize.cpp

@@ -101,11 +101,8 @@ namespace euf {
 
     void solver::attach_node(euf::enode* n) {
         expr* e = n->get_expr();
-        sat::literal lit;
-        if (!m.is_bool(e))
-            drat_log_node(e);
-        else 
-            lit = attach_lit(literal(si.add_bool_var(e), false), e);
+        if (m.is_bool(e))
+            attach_lit(literal(si.add_bool_var(e), false), e);
 
         if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) {
             auto* e_ext = expr2solver(e);

src/sat/smt/euf_proof.cpp

@@ -27,9 +27,7 @@ namespace euf {
         m_drat_initialized = true;
     }
 
-    void solver::drat_log_node(expr* e) {
-        if (!use_drat())
-            return;
+    void solver::drat_log_expr1(expr* e) {
         if (is_app(e)) {
             app* a = to_app(e);
             drat_log_decl(a->get_decl());
@@ -43,12 +41,41 @@ namespace euf {
             for (expr* arg : *a)
                 get_drat().def_add_arg(arg->get_id());
             get_drat().def_end();
+            m_drat_asts.insert(e);
+            push(insert_obj_trail<solver, ast>(m_drat_asts, e));
         }
         else {
             IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
         }
     }
 
+    void solver::drat_log_expr(expr* e) {
+        if (m_drat_asts.contains(e))
+            return;
+        ptr_vector<expr>::scoped_stack _sc(m_drat_todo);
+        m_drat_todo.push_back(e);
+        while (!m_drat_todo.empty()) {
+            e = m_drat_todo.back();
+            unsigned sz = m_drat_todo.size();
+            if (is_app(e)) 
+                for (expr* arg : *to_app(e))
+                    if (!m_drat_asts.contains(arg))
+                        m_drat_todo.push_back(arg);
+            if (m_drat_todo.size() != sz)
+                continue;
+            drat_log_expr1(e);
+            m_drat_todo.pop_back();                   
+        }
+    }
+
+    void solver::drat_bool_def(sat::bool_var v, expr* e) {
+        if (!use_drat())
+            return;
+        drat_log_expr(e);
+        get_drat().bool_def(v, e->get_id());
+    }
+
+
     void solver::drat_log_decl(func_decl* f) {
         if (f->get_family_id() != null_family_id) 
             return;

src/sat/smt/euf_solver.h

@@ -157,6 +157,9 @@ namespace euf {
         void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
         void log_antecedents(literal l, literal_vector const& r);
         void drat_log_decl(func_decl* f);
+        void drat_log_expr(expr* n);
+        void drat_log_expr1(expr* n);
+        ptr_vector<expr> m_drat_todo;
         obj_hashtable<ast> m_drat_asts;
         bool m_drat_initialized{ false };
         void init_drat();
@@ -289,6 +292,7 @@ namespace euf {
 
         bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
         sat::drat& get_drat() { return s().get_drat(); }
+        void drat_bool_def(sat::bool_var v, expr* n);
 
         // decompile
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
@@ -310,7 +314,6 @@ namespace euf {
         void unhandled_function(func_decl* f);
         th_rewriter& get_rewriter() { return m_rewriter; }
         bool is_shared(euf::enode* n) const;
-        void drat_log_node(expr* n);
 
         // relevancy
         bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; }

src/sat/smt/sat_smt.h

@@ -28,13 +28,6 @@ namespace sat {
         eframe(expr* e) : m_e(e), m_idx(0) {}
     };
 
-    struct scoped_stack {
-        svector<eframe>& s;
-        unsigned sz;
-        scoped_stack(svector<eframe>& s):s(s), sz(s.size()) {}
-        ~scoped_stack() { s.shrink(sz); }
-    };
-
     class sat_internalizer {
     public:
         virtual ~sat_internalizer() {}

src/sat/smt/sat_th.cpp

@@ -24,7 +24,7 @@ namespace euf {
     bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root, bool redundant) {
         IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(a, m) << "\n");
         flet<bool> _is_learned(m_is_redundant, redundant);
-        sat::scoped_stack _sc(m_stack);
+        svector<sat::eframe>::scoped_stack _sc(m_stack);
         unsigned sz = m_stack.size();
         visit(a);
         while (m_stack.size() > sz) {

src/sat/tactic/goal2sat.cpp

@@ -58,7 +58,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     };
     ast_manager &               m;
     pb_util                     pb;
-    sat::cut_simplifier*        m_aig;
     svector<frame>              m_frame_stack;
     svector<sat::literal>       m_result_stack;
     obj_map<app, sat::literal>  m_cache;
@@ -83,7 +82,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
         m(_m),
         pb(m),
-        m_aig(nullptr),
         m_solver(s),
         m_map(map),
         m_dep2asm(dep2asm),
@@ -92,11 +90,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_default_external(default_external) {
         updt_params(p);
         m_true = sat::null_literal;
-        m_aig = s.get_cut_simplifier();
     }
 
     ~imp() override {}
 
+
+    sat::cut_simplifier* aig() {
+        return m_solver.get_cut_simplifier();
+    }
+
     void updt_params(params_ref const & p) {
         sat_params sp(p);
         m_ite_extra  = p.get_bool("ite_extra", true);
@@ -178,27 +180,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (m_expr2var_replay && m_expr2var_replay->find(n, v))
             return v;
         v = m_solver.add_var(is_ext);
-        log_node(n);
         log_def(v, n);
         if (top_level_relevant() && !is_bool_op(n))
             ensure_euf()->track_relevancy(v);
         return v;
     }
 
     void log_def(sat::bool_var v, expr* n) {
-        if (m_drat && m_solver.get_drat_ptr()) 
-            m_solver.get_drat_ptr()->bool_def(v, n->get_id());
-    }
-
-    void log_node(expr* n) {
-        if (m_drat && m_solver.get_drat_ptr()) {
-            if (is_app(n)) {
-                for (expr* arg : *to_app(n))
-                    if (m.is_not(arg))
-                        log_node(arg);
-            }
-            ensure_euf()->drat_log_node(n);
-        }
+        if (m_drat && m_euf)
+            ensure_euf()->drat_bool_def(v, n);
     }
 
     sat::literal mk_true() {
@@ -413,15 +403,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
             m_result_stack.push_back(~l);
             lits = m_result_stack.end() - num - 1;
-            if (m_aig) {
+            if (aig()) {
                 aig_lits.reset();
                 aig_lits.append(num, lits);
             }
             // remark: mk_clause may perform destructive updated to lits.
             // I have to execute it after the binary mk_clause above.
             mk_clause(num+1, lits);
-            if (m_aig) 
-                m_aig->add_or(l, num, aig_lits.c_ptr());
+            if (aig()) 
+                aig()->add_or(l, num, aig_lits.c_ptr());
 
             m_solver.set_phase(~l);               
             m_result_stack.shrink(old_sz);
@@ -468,13 +458,13 @@ struct goal2sat::imp : public sat::sat_internalizer {
             }
             m_result_stack.push_back(l);
             lits = m_result_stack.end() - num - 1;
-            if (m_aig) {
+            if (aig()) {
                 aig_lits.reset();
                 aig_lits.append(num, lits);
             }
             mk_clause(num+1, lits);
-            if (m_aig) {
-                m_aig->add_and(l, num, aig_lits.c_ptr());
+            if (aig()) {
+                aig()->add_and(l, num, aig_lits.c_ptr());
             }        
             m_solver.set_phase(l);               
             if (sign)
@@ -516,7 +506,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 mk_clause(~t, ~e, l);
                 mk_clause(t,  e, ~l);
             }
-            if (m_aig) m_aig->add_ite(l, c, t, e);
+            if (aig()) aig()->add_ite(l, c, t, e);
             if (sign)
                 l.neg();
 
@@ -581,7 +571,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             mk_clause(~l, ~l1, l2);
             mk_clause(l,  l1, l2);
             mk_clause(l, ~l1, ~l2);
-            if (m_aig) m_aig->add_iff(l, l1, l2);            
+            if (aig()) aig()->add_iff(l, l1, l2);            
             if (sign)
                 l.neg();
             m_result_stack.push_back(l);

src/shell/drat_frontend.cpp

@@ -150,7 +150,7 @@ class smt_checker {
             check_assertion_redundant(lits);
         else if (!st.is_sat() && !st.is_deleted()) 
             check_clause(lits);        
-        m_drat.add(lits, st);
+        // m_drat.add(lits, st);
     }    
 
     /**
@@ -201,6 +201,19 @@ class smt_checker {
                     result = dtu.mk_is(f, args[0]);
                     return;
                 }
+                if (name == "Real" && sz == 4) {
+                    arith_util au(m);
+                    rational num = sexpr->get_child(2)->get_numeral();
+                    rational den = sexpr->get_child(3)->get_numeral();
+                    result = au.mk_numeral(num/den, false);
+                    return;
+                }
+                if (name == "Int" && sz == 3) {
+                    arith_util au(m);
+                    rational num = sexpr->get_child(2)->get_numeral();
+                    result = au.mk_numeral(num, true);
+                    return;
+                }
                 for (unsigned i = 2; i < sz; ++i) {
                     auto* child = sexpr->get_child(i);
                     if (child->is_numeral() && child->get_numeral().is_unsigned())

src/smt/theory_lra.cpp

@@ -384,7 +384,7 @@ class theory_lra::imp {
                 vars.push_back(v);
                 ++index;
             }
-            else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r <= 10) {
+            else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r.is_pos() && r <= 10) {
                 theory_var v = internalize_power(to_app(n), to_app(n1), r.get_unsigned());
                 coeffs[vars.size()] = coeffs[index];
                 vars.push_back(v);

src/smt/user_propagator.cpp

@@ -121,8 +121,12 @@ void user_propagator::propagate() {
             m_lits.append(m_id2justification[id]);
         for (auto const& p : prop.m_eqs)
             m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
-        DEBUG_CODE(for (auto const& p : m_eqs) SASSERT(p.first->get_root() == p.second->get_root()););
-
+        DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
+        IF_VERBOSE(5, 
+                   for (auto lit : m_lits) 
+                       verbose_stream() << lit << ":" << ctx.get_assignment(lit) << " ";
+                   verbose_stream() << "\n";);
+
         if (m.is_false(prop.m_conseq)) {
             js = ctx.mk_justification(
                 ext_theory_conflict_justification(

src/util/vector.h

@@ -596,6 +596,14 @@ class vector {
         if (s > size())
             resize(s);
     }
+
+    struct scoped_stack {
+        vector& s;
+        unsigned sz;
+        scoped_stack(vector& s):s(s), sz(s.size()) {}
+        ~scoped_stack() { s.shrink(sz); }
+    };
+
 };
 
 template<typename T>