fix bug in new core not detecting conflict, fix #6525, add tactic doc

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

src/ast/ast.cpp

@@ -1673,6 +1673,7 @@ bool ast_manager::are_distinct(expr* a, expr* b) const {
 }
 
 void ast_manager::add_lambda_def(func_decl* f, quantifier* q) {
+    TRACE("model", tout << "add lambda def " << mk_pp(q, *this) << "\n");
     m_lambda_defs.insert(f, q);
     f->get_info()->set_lambda(true);
     inc_ref(q);

src/ast/ast.h

@@ -1631,6 +1631,7 @@ class ast_manager {
     void add_lambda_def(func_decl* f, quantifier* q);
     quantifier* is_lambda_def(func_decl* f);
     quantifier* is_lambda_def(app* e) { return is_lambda_def(e->get_decl()); }
+    obj_map<func_decl, quantifier*> const& lambda_defs() const { return m_lambda_defs; }
 
     symbol const& lambda_def_qid() const { return m_lambda_def; }
 

src/ast/simplifiers/dependent_expr_state.cpp

@@ -83,6 +83,23 @@ void dependent_expr_state::freeze_recfun() {
     m_num_recfun = sz;
 }
 
+/**
+* Freeze all functions used in lambda defined declarations
+*/
+void dependent_expr_state::freeze_lambda() {
+    auto& m = m_frozen_trail.get_manager();
+    unsigned sz = m.lambda_defs().size();
+    if (m_num_lambdas >= sz)
+        return;
+
+    ast_mark visited;
+    for (auto const& [f, body] : m.lambda_defs()) 
+        freeze_terms(body, false, visited);
+    m_trail.push(value_trail(m_num_lambdas));
+    m_num_lambdas = sz;
+}
+
+
 /**
 * The current qhead is to be updated to qtail. 
 * Before this update, freeze all functions appearing in formulas.
@@ -100,8 +117,9 @@ void dependent_expr_state::freeze_suffix() {
     if (m_suffix_frozen)
         return;
     m_suffix_frozen = true;
-    auto& m = m_frozen_trail.get_manager();
     freeze_recfun();
+    freeze_lambda();
+    auto& m = m_frozen_trail.get_manager();
     ast_mark visited;
     ptr_vector<expr> es;
     for (unsigned i = qhead(); i < qtail(); ++i) {

src/ast/simplifiers/dependent_expr_state.h

@@ -43,12 +43,13 @@ Module Name:
 class dependent_expr_state {
     unsigned m_qhead = 0;
     bool     m_suffix_frozen = false;
-    unsigned m_num_recfun = 0;
+    unsigned m_num_recfun = 0, m_num_lambdas = 0;
     lbool    m_has_quantifiers = l_undef;
     ast_mark m_frozen;
     func_decl_ref_vector m_frozen_trail;
     void freeze_prefix();
     void freeze_recfun();
+    void freeze_lambda();
     void freeze_terms(expr* term, bool only_as_array, ast_mark& visited);
     void freeze(expr* term);
     void freeze(func_decl* f);

src/ast/simplifiers/solve_eqs.cpp

@@ -116,10 +116,10 @@ namespace euf {
                 for (auto const& eq : m_next[j]) {
                     auto const& [orig, v, t, d] = eq;
                     SASSERT(j == var2id(v));
-                    bool is_safe = true;
                     if (m_fmls.frozen(v))
                         continue;
 
+                    bool is_safe = true;                    
                     unsigned todo_sz = todo.size();
 
                     // determine if substitution is safe.
@@ -223,6 +223,8 @@ namespace euf {
 
     void solve_eqs::reduce() {
 
+        m_fmls.freeze_suffix();
+
         for (extract_eq* ex : m_extract_plugins)
             ex->pre_process(m_fmls);
 

src/nlsat/tactic/nlsat_tactic.h

@@ -13,7 +13,24 @@ Module Name:
 
     Leonardo (leonardo) 2012-01-02
 
-Notes:
+Tactic Documentation:
+
+## Tactic nlsat
+
+### Short Description
+
+(try to) solve goal using a nonlinear arithmetic solver
+
+### Example
+
+```z3
+(declare-const x Real)
+(declare-const y Real)
+(assert (> (* x x) (* y x)))
+(assert (> x 0))
+(assert (< y 1))
+(apply (then simplify purify-arith nlsat))
+```
 
 --*/
 #pragma once

src/nlsat/tactic/qfnra_nlsat_tactic.h

@@ -13,7 +13,26 @@ Module Name:
 
     Leonardo (leonardo) 2012-01-23
 
-Notes:
+Tactic Documentation:
+
+## Tactic qfnra-nlsat
+
+### Short Description
+
+Self-contained tactic that attempts to solve goal using a nonlinear arithmetic solver.
+It first applies tactics, such as `purify-arith` to convert the goal into a format
+where the `nlsat` tactic applies.
+
+### Example
+
+```z3
+(declare-const x Real)
+(declare-const y Real)
+(assert (> (* x x) (* y x)))
+(assert (> x 0))
+(assert (< y 1))
+(apply qfnra-nlsat)
+```
 
 --*/
 #pragma once

src/qe/qe_tactic.h

@@ -13,9 +13,33 @@ Module Name:
 
     Leonardo de Moura (leonardo) 2011-12-28.
 
-Revision History:
+Tactic Documentation
+
+## Tactic qe
+
+### Short Description
+
+Apply quantifier elimination on quantified sub-formulas.
+
+### Long Description
+
+The tactic applies quantifier elimination procedures on quantified sub-formulas.
+It relies on theory plugins that can perform quanifier elimination for selected theories.
+These plugins include Booleans, bit-vectors, arithmetic (linear), arrays, and data-types (term algebra).
+It performs feasibility checks on cases to throttle the set of sub-formulas where quantifier elimination
+is applied.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(assert (exists ((z Int)) (and (<= x (* 2 z)) (<= (* 3 z) y))))
+(apply qe)
+```
 
 --*/
+
 #pragma once
 
 #include "util/params.h"

src/sat/smt/arith_diagnostics.cpp

@@ -124,6 +124,19 @@ namespace arith {
         return m_arith_hint.mk(ctx);
     }
 
+    arith_proof_hint const* solver::explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
+        arith_proof_hint* hint = nullptr;
+        if (ctx.use_drat()) {
+            m_arith_hint.set_type(ctx, hint_type::farkas_h);
+            for (auto lit : core)
+                m_arith_hint.add_lit(rational::one(), lit);
+            for (auto const& [a,b] : eqs)
+                m_arith_hint.add_eq(a, b);
+            hint = m_arith_hint.mk(ctx);
+        }
+        return hint;
+    }
+
     arith_proof_hint const* solver::explain_implied_eq(lp::explanation const& e, euf::enode* a, euf::enode* b) {
         if (!ctx.use_drat())
             return nullptr;

src/sat/smt/arith_solver.cpp

@@ -1196,26 +1196,31 @@ namespace arith {
     void solver::set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
         reset_evidence();
         m_core.append(core);
-
-        ++m_num_conflicts;
-        ++m_stats.m_conflicts;
         for (auto ev : m_explanation)
             set_evidence(ev.ci());
+
         TRACE("arith",
             tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n";
             for (literal c : m_core) tout << literal2expr(c) << "\n";
             for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";);
-        DEBUG_CODE(
-            if (is_conflict) {
+
+        if (is_conflict) {
+            DEBUG_CODE(
                 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)
-            m_core.push_back(ctx.mk_literal(m.mk_eq(eq.first->get_expr(), eq.second->get_expr())));
-        for (literal& c : m_core)
-            c.neg();
-
-        add_redundant(m_core, explain(hint_type::farkas_h));
+                for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()));                       
+            ++m_num_conflicts;
+            ++m_stats.m_conflicts;
+            auto* hint = explain_conflict(m_core, m_eqs);
+            ctx.set_conflict(euf::th_explain::conflict(*this, m_core, m_eqs, hint));
+        }
+        else {
+            for (auto const& eq : m_eqs)
+                m_core.push_back(ctx.mk_literal(m.mk_eq(eq.first->get_expr(), eq.second->get_expr())));
+            for (literal& c : m_core)
+                c.neg();
+
+            add_redundant(m_core, explain(hint_type::farkas_h));
+        }
     }
 
     bool solver::is_infeasible() const {

src/sat/smt/arith_solver.h

@@ -478,6 +478,7 @@ namespace arith {
         arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal);
         arith_proof_hint const* explain_implied_eq(lp::explanation const& e, euf::enode* a, euf::enode* b);
         arith_proof_hint const* explain_trichotomy(sat::literal le, sat::literal ge, sat::literal eq);
+        arith_proof_hint const* explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
         void explain_assumptions(lp::explanation const& e);
 
 

src/sat/tactic/sat_tactic.h

@@ -13,7 +13,36 @@ Module Name:
 
     Leonardo (leonardo) 2011-10-26
 
-Notes:
+Tactic Documentation:
+
+## Tactic sat
+
+### Short Description
+
+Try to solve goal using a SAT solver
+
+## Tactic sat-preprocess
+
+### Short Description 
+
+Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution).
+
+### Example
+
+```z3
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+(declare-const d Bool)
+(declare-const e Bool)
+(declare-const f Bool)
+(declare-fun p (Bool) Bool)
+(assert (=> a b))
+(assert (=> b c))
+(assert a)
+(assert (not c))
+(apply sat-preprocess)
+```
 
 --*/
 #pragma once

src/smt/tactic/ctx_solver_simplify_tactic.h

@@ -13,7 +13,17 @@ Module Name:
 
     Nikolaj (nbjorner) 2012-3-6
 
-Notes:
+Tactic Documentation:
+
+## Tactic ctx-solver-simplify
+
+### Short Description
+
+A heavy handed version of `ctx-simplify`. It applies SMT checks on sub-formulas to check
+if they can be simplified to `true` or `false` within their context.
+Note that a sub-formula may occur within multiple contexts due to shared sub-terms.
+In this case the tactic is partial and simplifies a limited number of context occurrences.
+
 
 --*/
 #pragma once

src/smt/tactic/unit_subsumption_tactic.h

@@ -13,12 +13,20 @@ Module Name:
 
     Nikolaj Bjorner (nbjorner) 2012-9-6
 
-Notes:
+Tactic Documentation:
 
-    Background: PDR generates several clauses that subsume each-other.
-    Simplify a goal assuming it is a conjunction of clauses.
-    Subsumed clauses are simplified by using unit-propagation 
-    It uses the smt_context for the solver.
+## Tactic unit-subsume-simplify
+
+### Short Description
+
+implify goal using subsumption based on unit propagation
+
+### Long Description
+
+Background: PDR generates several clauses that subsume each-other.
+Simplify a goal assuming it is a conjunction of clauses.
+Subsumed clauses are simplified by using unit-propagation 
+It uses the default SMT solver.
 
 --*/
 #pragma once