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

src/ast/csp_decl_plugin.cpp

@@ -104,7 +104,7 @@ func_decl * csp_decl_plugin::mk_func_decl(
         if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-job-resource expects should be an integer");
         if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-job-resource expects should be an integer");
         if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-job-resource expects should be an integer");
-        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be an a list of properties");
+        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be a list of properties");
         name = symbol("add-job-resource");
         rng = m_alist_sort;
         break;
@@ -115,7 +115,7 @@ func_decl * csp_decl_plugin::mk_func_decl(
         if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer");
         if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer");
         if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-resource-available expects should be an integer");
-        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-resource-available should be an a list of properties");
+        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-resource-available should be a list of properties");
         name = symbol("add-resource-available");
         rng = m_alist_sort;
         break;

src/muz/rel/dl_relation_manager.h

@@ -263,7 +263,7 @@ namespace datalog {
         }
 
         /**
-            \brief Return an operation that is a composition of a join an a project operation.
+            \brief Return an operation that is a composition of a join and a project operation.
         */
         relation_join_fn * mk_join_project_fn(const relation_base & t1, const relation_base & t2,
                 unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, 
@@ -433,7 +433,7 @@ namespace datalog {
         }
 
         /**
-            \brief Return an operation that is a composition of a join an a project operation.
+            \brief Return an operation that is a composition of a join and a project operation.
 
             This operation is equivalent to the two operations performed separately, unless functional 
             columns are involved.

src/muz/spacer/spacer_context.cpp

@@ -2366,11 +2366,6 @@ void context::updt_params() {
     }
 }
 
-void context::display_certificate(std::ostream& out) const {
-    proof_ref pr = get_proof();
-    out << pr;
-}
-
 void context::reset()
 {
     TRACE("spacer", tout << "\n";);
@@ -2507,7 +2502,7 @@ void context::add_cover(int level, func_decl* p, expr* property, bool bg)
 }
 
 void context::add_invariant (func_decl *p, expr *property)
-{add_cover (infty_level(), p, property, true);}
+{add_cover (infty_level(), p, property, use_bg_invs());}
 
 expr_ref context::get_reachable(func_decl *p) {
     pred_transformer* pt = nullptr;
@@ -2747,7 +2742,7 @@ lbool context::solve(unsigned from_lvl)
     if (m_last_result == l_true) {
         m_stats.m_cex_depth = get_cex_depth ();
     }
- 
+
     if (m_params.print_statistics ()) {
         statistics st;
         collect_statistics (st);
@@ -2931,10 +2926,6 @@ expr_ref context::get_answer()
     }
 }
 
-/**
-   \brief Retrieve satisfying assignment with explanation.
-*/
-expr_ref context::mk_sat_answer() {return get_ground_sat_answer();}
 
 
 expr_ref context::mk_unsat_answer() const
@@ -2957,8 +2948,7 @@ proof_ref context::get_ground_refutation() {
     ground_sat_answer_op op(*this);
     return op(*m_query);
 }
-expr_ref context::get_ground_sat_answer()
-{
+expr_ref context::get_ground_sat_answer() const {
     if (m_last_result != l_true) {
         IF_VERBOSE(0, verbose_stream()
                    << "Sat answer unavailable when result is false\n";);
@@ -3086,6 +3076,20 @@ expr_ref context::get_ground_sat_answer()
     return expr_ref(m.mk_and(cex.size(), cex.c_ptr()), m);
 }
 
+void context::display_certificate(std::ostream &out) const {
+    switch(m_last_result) {
+    case l_false:
+        out << mk_pp(mk_unsat_answer(), m);
+        break;
+    case l_true:
+        out << mk_pp(mk_sat_answer(), m);
+        break;
+    case l_undef:
+        out << "unknown";
+        break;
+    }
+}
+
 ///this is where everything starts
 lbool context::solve_core (unsigned from_lvl)
 {

src/muz/spacer/spacer_context.h

@@ -1007,7 +1007,10 @@ class context {
                          const vector<bool>& reach_pred_used,
                          pob_ref_buffer &out);
 
-    expr_ref mk_sat_answer();
+    /**
+       \brief Retrieve satisfying assignment with explanation.
+    */
+    expr_ref mk_sat_answer() const {return get_ground_sat_answer();}
     expr_ref mk_unsat_answer() const;
     unsigned get_cex_depth ();
 
@@ -1083,7 +1086,7 @@ public:
      * get bottom-up (from query) sequence of ground predicate instances
      * (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query
      */
-    expr_ref get_ground_sat_answer ();
+    expr_ref get_ground_sat_answer () const;
     proof_ref get_ground_refutation();
     void get_rules_along_trace (datalog::rule_ref_vector& rules);
 

src/muz/spacer/spacer_generalizers.cpp

@@ -107,8 +107,7 @@ void lemma_bool_inductive_generalizer::operator()(lemma_ref &lemma) {
             expand_literals(m, extra_lits);
             SASSERT(extra_lits.size() > 0);
             bool found = false;
-            if (extra_lits.get(0) != lit) {
-                SASSERT(extra_lits.size() > 1);
+            if (extra_lits.get(0) != lit && extra_lits.size() > 1) {
                 for (unsigned j = 0, sz = extra_lits.size(); !found && j < sz; ++j) {
                     cube[i] = extra_lits.get(j);
                     if (pt.check_inductive(lemma->level(), cube, uses_level, weakness)) {

src/smt/theory_jobscheduler.cpp

@@ -315,7 +315,7 @@ namespace smt {
 
     /**
      *  For time interval [t0, t1] the end-time can be computed as a function 
-     *  of start time based on reource load availability.
+     *  of start time based on resource load availability.
      * 
      *  r = resource(j) & t1 >= start(j) >= t0 => end(j) = start(j) + ect(j, r, t0) - t0
      */
@@ -672,7 +672,7 @@ namespace smt {
     }
 
     /*
-     * Initialze the state based on the set of jobs and resources added.
+     * Initialize the state based on the set of jobs and resources added.
      * Ensure that the availability slots for each resource is sorted by time.
      *
      * For each resource j: