Merge branch 'synth' of https://github.com/z3prover/z3 into synth

src/ast/for_each_expr.cpp

@@ -109,9 +109,9 @@ bool has_skolem_functions(expr * n) {
 
 subterms::subterms(expr_ref_vector const& es, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp): m_include_bound(include_bound), m_es(es), m_esp(esp), m_vp(vp) {}
 subterms::subterms(expr_ref const& e, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp) : m_include_bound(include_bound), m_es(e.m()), m_esp(esp), m_vp(vp) { if (e) m_es.push_back(e); }
-subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); }
+subterms::iterator subterms::begin() const { return iterator(* this, m_esp, m_vp, true); }
-subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); }
+subterms::iterator subterms::end() const { return iterator(*this, nullptr, nullptr, false); }
-subterms::iterator::iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
+subterms::iterator::iterator(subterms const& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
     if (!esp)
         m_esp = &m_es;
     else

src/ast/for_each_expr.h

@@ -186,7 +186,7 @@ public:
         expr_mark         m_visited;   
         expr_mark*        m_visitedp = nullptr;
     public:
-        iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
+        iterator(subterms const& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
         expr* operator*();
         iterator operator++(int);
         iterator& operator++();
@@ -198,8 +198,8 @@ public:
     static subterms ground(expr_ref const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
     static subterms all(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); }
     static subterms ground(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
-    iterator begin();
+    iterator begin() const;
-    iterator end();
+    iterator end() const;
 };
 
 class subterms_postorder {

src/sat/smt/synth_solver.cpp

@@ -23,88 +23,71 @@ namespace synth {
         
     solver::~solver() {}
 
-
-    // recognize synthesis objective as part of search objective.
-    // register it for calls to check.
-    void solver::asserted(sat::literal lit) {
-
-    }
-
     bool solver::contains_uncomputable(expr* e) {
 	return false;
     }
 
-    bool solver::synthesize(app* e) {
+    sat::literal solver::synthesize(app* e) {
 
         if (e->get_num_args() == 0)
-            return false;
+            return sat::null_literal;
         
 	auto * n = expr2enode(e->get_arg(0));
 	expr_ref_vector repr(m);
-	euf::enode_vector todo;
-        auto has_rep = [&](euf::enode* n) { return !!repr.get(n->get_root_id(), nullptr); };
         auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); };
+        auto has_rep = [&](euf::enode* n) { return !!get_rep(n); };
+        auto set_rep = [&](euf::enode* n, expr* e) { repr.setx(n->get_root_id(), e); };
+        auto is_computable = [&](func_decl* f) { return true; };
+
+	euf::enode_vector todo;                
+        
 	for (unsigned i = 1; i < e->get_num_args(); ++i) {
 	    expr * arg = e->get_arg(i);
 	    auto * narg = expr2enode(arg);
 	    todo.push_back(narg);
-	    repr.setx(narg->get_root_id(), arg);
+	    set_rep(narg, arg);
         }
 	for (unsigned i = 0; i < todo.size() && !has_rep(n); ++i) {
 	    auto * nn = todo[i];
             for (auto * p : euf::enode_parents(nn)) {
 	        if (has_rep(p))
                     continue;
-                if (all_of(euf::enode_args(p), [&](auto * ch) { return has_rep(ch); })) {
+                if (!is_computable(p->get_decl()))
+                    continue;
+                if (!all_of(euf::enode_args(p), [&](auto * ch) { return has_rep(ch); }))
+                    continue;
                 ptr_buffer<expr> args;
                 for (auto * ch : euf::enode_args(p))
                     args.push_back(get_rep(ch));
                 app * papp = m.mk_app(p->get_decl(), args);
-	            repr.setx(p->get_root_id(), papp);
+                set_rep(p, papp);
                 todo.push_back(p);
             }
 	}
-        }
 	expr * sol = get_rep(n);
         if (!sol)
-            return false;
+            return sat::null_literal;
 
-        sat::literal lit = eq_internalize(n->get_expr(), sol);
-        add_unit(~lit);
         IF_VERBOSE(0, verbose_stream() << mk_pp(sol, m) << "\n");
-        return true;
+        return eq_internalize(n->get_expr(), sol);
     }
 
     // block current model using realizer by E-graph (and arithmetic)
     // 
     sat::check_result solver::check() {
-    for (app* e : m_synth)
+        sat::literal_vector clause;
-        if (synthesize(e))
+	for (app* e : m_synth) {
-               sat::check_result::CR_CONTINUE; 
+	    auto lit = synthesize(e);
+            if (lit == sat::null_literal)
+                return sat::check_result::CR_GIVEUP;
+            clause.push_back(~lit);
+        }
+        if (clause.empty())
             return sat::check_result::CR_DONE;
+        add_clause(clause);
+        return sat::check_result::CR_CONTINUE; 
     }
 
-    // nothing particular to do
-    void solver::push_core() {
-
-    }
-
-    // nothing particular to do
-    void solver::pop_core(unsigned n) {
-    }
-
-    // nothing particular to do
-    bool solver::unit_propagate() {
-        return false;
-    }
-
-    // retrieve explanation for assertions made by synth solver. It only asserts unit literals so nothing to retrieve
-    void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) {
-    }
-
-    // where we collect statistics (number of invocations?)
-    void solver::collect_statistics(statistics& st) const {}
-
     void solver::add_uncomputable(app* e) {
         for (unsigned i = 0; i < e->get_num_args(); ++i) {
 	    expr* a = e->get_arg(i);
@@ -140,22 +123,14 @@ namespace synth {
 
     // display current state (eg. current set of realizers)
     std::ostream& solver::display(std::ostream& out) const {
+        for (auto * e : m_synth)
+            out << "synth objective " << mk_pp(e, m) << "\n";            
         return out;
     }
 
-    // justified by "synth".
-    std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const {
-        return out << "synth";
-    }
-    
-    std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
-        return out << "synth";
-    }
-
     // create a clone of the solver.
     euf::th_solver* solver::clone(euf::solver& ctx) {
-        NOT_IMPLEMENTED_YET();
+        return alloc(solver, ctx);
-        return nullptr;
     }
 
 }

src/sat/smt/synth_solver.h

@@ -22,30 +22,25 @@ Author:
 namespace synth {
 
     class solver : public euf::th_euf_solver {
-
     public:
         solver(euf::solver& ctx);
-        
         ~solver() override;        
-
+        void asserted(sat::literal lit) override {}
-        
-        void asserted(sat::literal lit) override;
-
         sat::check_result check() override;
-        void push_core() override;
+        void push_core() override {}
-        void pop_core(unsigned n) override;
+        void pop_core(unsigned n) override {}
-        bool unit_propagate() override;
+        bool unit_propagate() override { return false; }
-        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override;
+        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override {}
-        void collect_statistics(statistics& st) const override;
+        void collect_statistics(statistics& st) const override {}
         sat::literal internalize(expr* e, bool sign, bool root) override;
         void internalize(expr* e) override;
         std::ostream& display(std::ostream& out) const override;
-        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
+        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return out << "synth"; }
-        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out << "synth"; }
         euf::th_solver* clone(euf::solver& ctx) override;
 
     private:
-	bool synthesize(app* e);
+        sat::literal synthesize(app* e);
 	void add_uncomputable(app* e);
 	bool contains_uncomputable(expr* e);
 

src/util/util.h

@@ -363,7 +363,7 @@ void set_fatal_error_handler(void (*pfn)(int error_code));
 
 
 template<typename S, typename T>
-bool any_of(S& set, T const& p) {
+bool any_of(S const & set, T const& p) {
     for (auto const& s : set)
         if (p(s))
             return true;
@@ -371,7 +371,7 @@ bool any_of(S& set, T const& p) {
 }
 
 template<typename S, typename T>
-bool all_of(S& set, T const& p) {
+bool all_of(S const & set, T const& p) {
     for (auto const& s : set)
         if (!p(s))
             return false;