checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/smt/ctx_solver_simplify_tactic.cpp

@@ -0,0 +1,284 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    ctx_solver_simplify_tactic.cpp
+
+Abstract:
+
+    Context simplifier for propagating solver assignments.
+
+Author:
+
+    Nikolaj (nbjorner) 2012-3-6
+
+Notes:
+
+--*/
+
+#include"ctx_solver_simplify_tactic.h"
+#include"arith_decl_plugin.h"
+#include"front_end_params.h"
+#include"smt_solver.h"
+#include"ast_pp.h"
+#include"mk_simplified_app.h"
+
+
+class ctx_solver_simplify_tactic : public tactic {
+    ast_manager&          m;
+    params_ref            m_params;
+    front_end_params      m_front_p;
+    smt::solver           m_solver;
+    arith_util            m_arith;
+    mk_simplified_app     m_mk_app;
+    func_decl_ref         m_fn;
+    unsigned              m_num_steps;
+public:
+    ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()):
+        m(m), m_params(p), m_solver(m, m_front_p),  m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0) {
+        sort* i_sort = m_arith.mk_int();
+        m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort());
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(ctx_solver_simplify_tactic, m, m_params);
+    }
+
+    virtual ~ctx_solver_simplify_tactic() {}
+
+    virtual void updt_params(params_ref const & p) {
+        m_solver.updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) { 
+        m_solver.collect_param_descrs(r); 
+    }
+    
+    virtual void collect_statistics(statistics & st) const {
+        st.update("solver-simplify-steps", m_num_steps);
+    }
+
+    virtual void reset_statistics() { m_num_steps = 0; }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        
+        mc = 0; pc = 0; core = 0;
+        reduce(*(in.get()));
+        in->inc_depth();
+        result.push_back(in.get());
+    }
+
+    virtual void cleanup() {
+        reset_statistics();
+        m_solver.reset();
+    }
+protected:
+    virtual void set_cancel(bool f) {
+        m_solver.set_cancel(f);
+    }
+
+    void reduce(goal& g) {
+        SASSERT(g.is_well_sorted());
+        bool proofs_enabled = g.proofs_enabled();
+        m_num_steps = 0;
+        expr_ref fml(m);
+        tactic_report report("ctx-solver-simplify", g);
+        unsigned sz = g.size();
+        if (g.inconsistent())
+            return;
+        ptr_vector<expr> fmls;
+        g.get_formulas(fmls);
+        fml = m.mk_and(fmls.size(), fmls.c_ptr());
+        reduce(fml);
+        g.reset();
+        g.assert_expr(fml, 0, 0); 
+        IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-solver-simplify :num-steps " << m_num_steps << ")\n";);
+        SASSERT(g.is_well_sorted());        
+    }
+
+    void reduce(expr_ref& result){
+        SASSERT(m.is_bool(result));
+        ptr_vector<expr> todo;
+        ptr_vector<expr> names;
+        svector<bool>    is_checked;
+        svector<unsigned> parent_ids, self_ids;
+        expr_ref_vector fresh_vars(m), trail(m);
+        expr_ref res(m);
+        obj_map<expr,std::pair<unsigned, expr*> > cache;
+        unsigned id = 1;
+        expr* n = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
+        expr* n2, *fml;
+        unsigned path_id = 0, self_pos = 0;
+        app * a;
+        unsigned sz;
+        std::pair<unsigned,expr*> path_r;
+        ptr_vector<expr> found;
+
+        fml = result.get();
+        m_solver.assert_expr(m.mk_not(m.mk_iff(fml, n)));
+
+        trail.push_back(n);        
+        todo.push_back(fml);
+        names.push_back(n);
+        is_checked.push_back(false);
+        parent_ids.push_back(0);
+        self_ids.push_back(0);        
+        m_solver.push();
+
+        while (!todo.empty()) {            
+            expr_ref res(m);
+            ptr_buffer<expr> args;
+            expr* e = todo.back();
+            unsigned pos = parent_ids.back();
+            n = names.back();
+            bool checked = is_checked.back();
+            
+            if (cache.contains(e)) {
+                goto done;
+            }
+            if (!m.is_bool(e)) {
+                res = e;
+                goto done;
+            }
+            if (m.is_bool(e) && !checked && simplify_bool(n, res)) {
+                goto done;
+            }
+            if (!is_app(e)) {
+                res = e;
+                goto done;
+            }
+            
+            a = to_app(e);
+            if (!is_checked.back()) {
+                self_ids.back() = ++path_id;
+                is_checked.back() = true;
+            }
+            self_pos = self_ids.back();
+            sz = a->get_num_args();
+            
+            n2 = 0;
+
+            found.reset(); // arguments already simplified.
+            for (unsigned i = 0; i < sz; ++i) {
+                expr* arg = a->get_arg(i);
+                if (!m.is_bool(arg)) {
+                    args.push_back(arg);
+                }
+                else if (cache.find(arg, path_r) && !found.contains(arg)) {
+                    //
+                    // This is a single traversal version of the context
+                    // simplifier. It simplifies only the first occurrence of 
+                    // a formula with respect to the context.
+                    //
+                                        
+                    found.push_back(arg);
+                    if (path_r.first == self_pos) {
+                        TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << "\n";);
+                        args.push_back(path_r.second);
+                    }
+                    else {
+                        res = local_simplify(a, n, id, i);
+                        TRACE("ctx_solver_simplify_tactic", 
+                              tout << "Already cached: " << path_r.first << " " << mk_pp(res, m) << "\n";);
+                        args.push_back(arg);
+                    }
+                }
+                else if (!n2 && !found.contains(arg)) {                
+                    n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
+                    todo.push_back(arg);
+                    parent_ids.push_back(self_pos);
+                    self_ids.push_back(0);
+                    names.push_back(n2);
+                    trail.push_back(n2);
+                    args.push_back(n2);
+                    is_checked.push_back(false);
+                }
+                else {
+                    args.push_back(arg);
+                }
+            }
+            m_mk_app(a->get_decl(), args.size(), args.c_ptr(), res);
+            trail.push_back(res);
+            // child needs to be visited.
+            if (n2) {
+                m_solver.push();
+                m_solver.assert_expr(m.mk_eq(res, n));
+                continue;
+            }
+        
+        done:
+            if (res) {
+                cache.insert(e, std::make_pair(pos, res));
+            }
+            
+            TRACE("ctx_solver_simplify_tactic",
+                  tout << mk_pp(e, m) << " checked: " << checked << " cached: " << mk_pp(res?res.get():e, m) << "\n";);
+            
+            todo.pop_back();
+            parent_ids.pop_back();
+            self_ids.pop_back();
+            names.pop_back();
+            is_checked.pop_back();
+            m_solver.pop(1);
+        }
+        VERIFY(cache.find(fml, path_r));
+        result = path_r.second;
+    }
+
+    bool simplify_bool(expr* n, expr_ref& res) {
+
+        m_solver.push();
+        m_solver.assert_expr(n);
+        lbool is_sat = m_solver.check();
+        m_solver.pop(1);
+        if (is_sat == l_false) {
+            res = m.mk_true();
+            return true;
+        }
+
+        m_solver.push();
+        m_solver.assert_expr(m.mk_not(n));
+        is_sat = m_solver.check();
+        m_solver.pop(1);
+        if (is_sat == l_false) {
+            res = m.mk_false();
+            return true;
+        }
+
+        return false;
+    }
+
+    expr_ref local_simplify(app* a, expr* n, unsigned& id, unsigned index) {
+        SASSERT(index < a->get_num_args());
+        SASSERT(m.is_bool(a->get_arg(index)));
+        expr_ref n2(m), result(m);
+        n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
+        ptr_buffer<expr> args;
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            if (i == index) {
+                args.push_back(n2);
+            }
+            else {
+                args.push_back(a->get_arg(i));
+            }
+        }
+        m_mk_app(a->get_decl(), args.size(), args.c_ptr(), result);
+        m_solver.push();
+        m_solver.assert_expr(m.mk_eq(result, n));
+        if (!simplify_bool(n2, result)) {
+            result = a;
+        }
+        m_solver.pop(1);
+        return result;
+    }
+    
+};
+
+tactic * mk_ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(ctx_solver_simplify_tactic, m, p));
+}

src/smt/ctx_solver_simplify_tactic.h

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    ctx_solver_simplify_tactic.h
+
+Abstract:
+
+    Context simplifier for propagating solver assignments.
+
+Author:
+
+    Nikolaj (nbjorner) 2012-3-6
+
+Notes:
+
+--*/
+#ifndef _CTX_SOLVER_SIMPLIFY_TACTIC_H_
+#define _CTX_SOLVER_SIMPLIFY_TACTIC_H_
+
+#include"tactical.h"
+
+tactic * mk_ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif

src/smt/mk_database.sh

@@ -0,0 +1,3 @@
+#!/bin/sh
+dos2unix database.smt
+./gen database.smt | awk 'BEGIN { print "char const * g_pattern_database =" } { print "\"" $0 "\\n\"" } END { print ";" }' > database.h

src/smt/ni_solver.cpp

@@ -0,0 +1,236 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    ni_solver.cpp
+
+Abstract:
+    Wrappers for smt::solver that are non-incremental & (quasi-incremental).
+
+Author:
+
+    Leonardo (leonardo) 2011-03-30
+
+Notes:
+
+--*/
+#include"ni_solver.h"
+#include"smt_solver.h"
+#include"cmd_context.h"
+
+class ni_smt_solver : public solver {
+protected:
+    cmd_context &       m_cmd_ctx;
+    smt::solver *       m_context;
+    progress_callback * m_callback;
+public:
+    ni_smt_solver(cmd_context & ctx):m_cmd_ctx(ctx), m_context(0), m_callback(0) {}
+
+    virtual ~ni_smt_solver() {
+        if (m_context != 0)
+            dealloc(m_context);
+    }
+
+    virtual void init(ast_manager & m, symbol const & logic) {
+        // do nothing
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        if (m_context == 0) {
+            return;
+        }
+        else {
+            m_context->collect_statistics(st);
+        }
+    }
+
+    virtual void reset() {
+        if (m_context != 0) {
+            #pragma omp critical (ni_solver) 
+            {
+                dealloc(m_context);
+                m_context = 0;
+            }
+        }
+    }
+
+    virtual void assert_expr(expr * t) {
+        // do nothing
+    }
+
+    virtual void push() {
+        // do nothing
+    }
+
+    virtual void pop(unsigned n) {
+        // do nothing
+    }
+
+    virtual unsigned get_scope_level() const {
+        return m_cmd_ctx.num_scopes();
+    }
+
+    void assert_exprs() {
+        ptr_vector<expr>::const_iterator it  = m_cmd_ctx.begin_assertions();
+        ptr_vector<expr>::const_iterator end = m_cmd_ctx.end_assertions();
+        for (; it != end; ++it) {
+            m_context->assert_expr(*it);
+        }
+    }
+
+    void init_solver() {
+        reset();
+        #pragma omp critical (ni_solver)
+        {
+            m_context = alloc(smt::solver, m_cmd_ctx.m(), m_cmd_ctx.params());
+        }
+        if (m_cmd_ctx.has_logic())
+            m_context->set_logic(m_cmd_ctx.get_logic());
+        if (m_callback)
+            m_context->set_progress_callback(m_callback);
+        assert_exprs();
+    }
+
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
+        // erase current solver, and create a new one.
+        init_solver();
+
+        if (num_assumptions == 0) {
+            return m_context->setup_and_check();
+        }
+        else {
+            return m_context->check(num_assumptions, assumptions); 
+        }
+    }
+
+    virtual void get_unsat_core(ptr_vector<expr> & r) {
+        SASSERT(m_context);
+        unsigned sz = m_context->get_unsat_core_size();
+        for (unsigned i = 0; i < sz; i++)
+            r.push_back(m_context->get_unsat_core_expr(i));
+    }
+
+    virtual void get_model(model_ref & m) {
+        SASSERT(m_context);
+        m_context->get_model(m);
+    }
+
+    virtual proof * get_proof() {
+        SASSERT(m_context);
+        return m_context->get_proof();
+    }
+
+    virtual std::string reason_unknown() const {
+        SASSERT(m_context);
+        return m_context->last_failure_as_string();
+    }
+
+    virtual void get_labels(svector<symbol> & r) {
+        SASSERT(m_context);
+        buffer<symbol> tmp;
+        m_context->get_relevant_labels(0, tmp);
+        r.append(tmp.size(), tmp.c_ptr());
+    }
+
+    virtual void set_cancel(bool f) {
+        #pragma omp critical (ni_solver)
+        {
+            if (m_context)
+                m_context->set_cancel(f);
+        }
+    }
+
+    virtual void set_progress_callback(progress_callback * callback) {
+        m_callback = callback;
+        if (m_context)
+            m_context->set_progress_callback(callback);
+    }
+
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        smt::solver::collect_param_descrs(r);
+    }
+
+};
+
+solver * mk_non_incremental_smt_solver(cmd_context & ctx) {
+    return alloc(ni_smt_solver, ctx);
+}
+
+class qi_smt_solver : public ni_smt_solver {
+    bool            m_inc_mode;   
+public:
+    qi_smt_solver(cmd_context & ctx):ni_smt_solver(ctx), m_inc_mode(false) {}
+    
+    virtual ~qi_smt_solver() {}
+
+    virtual void init(ast_manager & m, symbol const & logic) {
+        if (m_inc_mode) {
+            init_solver();
+            m_inc_mode = true;
+        }
+    }
+
+    virtual void reset() {
+        ni_smt_solver::reset();
+        m_inc_mode = false;
+    }
+
+    void switch_to_inc() {
+        if (!m_inc_mode) {
+            init_solver();
+            m_inc_mode = true;
+        }
+        SASSERT(m_inc_mode);
+    }
+
+    virtual void assert_expr(expr * t) {
+        if (m_context != 0 && !m_inc_mode) {
+            // solver was already created to solve a check_sat query...
+            switch_to_inc();
+        }
+        if (m_inc_mode) {
+            SASSERT(m_context);
+            m_context->assert_expr(t);
+        }
+    }
+
+    virtual void push() {
+        switch_to_inc();
+        SASSERT(m_context);
+        m_context->push();
+        SASSERT(m_inc_mode);
+    }
+
+    virtual void pop(unsigned n) {
+        switch_to_inc();
+        SASSERT(m_context);
+        m_context->pop(n);
+        SASSERT(m_inc_mode);
+    }
+
+    virtual unsigned get_scope_level() const {
+        if (!m_inc_mode)
+            return 0;
+        else
+            return m_context->get_scope_level();
+    }
+
+
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
+        if (!m_inc_mode) {
+            lbool r = ni_smt_solver::check_sat(num_assumptions, assumptions);
+            SASSERT(!m_inc_mode);
+            return r;
+        }
+        else {
+            return m_context->check(num_assumptions, assumptions); 
+        }
+    }
+};
+
+
+solver * mk_quasi_incremental_smt_solver(cmd_context & ctx) {
+    return alloc(qi_smt_solver, ctx);
+}

src/smt/ni_solver.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    ni_solver.h
+
+Abstract:
+    Wrappers for smt::context that are non-incremental & (quasi-incremental).
+
+Author:
+
+    Leonardo (leonardo) 2011-03-30
+
+Notes:
+
+--*/
+#ifndef _NI_SOLVER_H_
+#define _NI_SOLVER_H_
+
+#include"solver.h"
+class cmd_context;
+
+// Creates a solver that restarts from scratch for every call to check_sat
+solver * mk_non_incremental_smt_solver(cmd_context & ctx);
+
+// Creates a solver that restarts from scratch for the first call to check_sat, and then moves to incremental behavior.
+solver * mk_quasi_incremental_smt_solver(cmd_context & ctx);
+
+#endif