still integrating duality

src/ast/ast.cpp

@@ -3152,4 +3152,11 @@ void scoped_mark::pop_scope(unsigned num_scopes) {
     }
 }
    
+// Added by KLM for use in GDB
+
+// show an expr_ref on stdout
+
+void prexpr(expr_ref &e){
+  std::cout << mk_pp(e.get(), e.get_manager()) << std::endl;
+}
 

src/duality/duality.h

@@ -156,10 +156,11 @@ namespace Duality {
 
            virtual
            lbool interpolate_tree(TermTree *assumptions,
-				     TermTree *&interpolants,
-			             model &_model,
-                                     TermTree *goals = 0
-			            ) = 0;
+				  TermTree *&interpolants,
+				  model &_model,
+				  TermTree *goals = 0,
+				  bool weak = false
+				  ) = 0;
            
            /** Assert a background axiom. */
            virtual void assert_axiom(const expr &axiom) = 0;
@@ -181,11 +182,13 @@ namespace Duality {
         interpolating_solver *islvr;   /** iZ3 solver */
 
         lbool interpolate_tree(TermTree *assumptions,
-				  TermTree *&interpolants,
-			          model &_model,
-                                  TermTree *goals = 0)
+			       TermTree *&interpolants,
+			       model &_model,
+			       TermTree *goals = 0,
+			       bool weak = false)
         {
            literals _labels;
+	   islvr->SetWeakInterpolants(weak);
            return islvr->interpolate_tree(assumptions,interpolants,_model,_labels,true);
         }
 

src/duality/duality_rpfp.cpp

@@ -585,7 +585,7 @@ namespace Duality {
     // if (dualLabels != null) dualLabels.Dispose();
     
     timer_start("interpolate_tree");
-    lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals);
+    lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals,true);
     timer_stop("interpolate_tree");
     if (res == l_false)
       {

src/duality/duality_solver.cpp

@@ -294,7 +294,9 @@ namespace Duality {
 
     /** Return the counterexample */
     virtual Counterexample GetCounterexample(){
-      return cex;
+      Counterexample res = cex;
+      cex.tree = 0; // Cex now belongs to caller
+      return res;
     }
 
     // options
@@ -879,6 +881,7 @@ namespace Duality {
 #endif
       if(_cex) *_cex = cex;
       else delete cex.tree;    // delete the cex if not required
+      cex.tree = 0;
       node->Bound = save; // put back original bound
       timer_stop("ProveConjecture");
       return false;

src/duality/duality_wrapper.cpp

@@ -467,14 +467,12 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     
     if(res == unsat){
 
-      // TODO
-#if 0
+      interpolation_options_struct opts;
       if(weak_mode)
-	Z3_set_interpolation_option(options,"weak","1"); 
-#endif
+	opts.set("weak","1"); 
       
       ::ast *proof = m_solver->get_proof();
-      iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,0);
+      iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
       
       std::vector<expr> linearized_interpolants(_interpolants.size());
       for(unsigned i = 0; i < _interpolants.size(); i++)

src/interp/iz3interp.cpp

@@ -323,6 +323,8 @@ void iz3interpolate(ast_manager &_m_manager,
 		    interpolation_options_struct * options)
 {
   iz3interp itp(_m_manager);
+  if(options)
+    options->apply(itp);
   std::vector<iz3mgr::ast> _cnsts(cnsts.size());
   std::vector<int> _parents(parents.size());
   std::vector<iz3mgr::ast> _interps;
@@ -348,6 +350,8 @@ void iz3interpolate(ast_manager &_m_manager,
 		    interpolation_options_struct * options)
 {
   iz3interp itp(_m_manager);
+  if(options)
+    options->apply(itp);
   std::vector<iz3mgr::ast> _cnsts(cnsts.size());
   std::vector<iz3mgr::ast> _interps;
   for(unsigned i = 0; i < cnsts.size(); i++)
@@ -369,6 +373,8 @@ lbool iz3interpolate(ast_manager &_m_manager,
 		     interpolation_options_struct * options)
 {
   iz3interp itp(_m_manager);
+  if(options)
+    options->apply(itp);
   iz3mgr::ast _tree = itp.cook(tree);
   std::vector<iz3mgr::ast> _cnsts;
   itp.assert_conjuncts(s,_cnsts,_tree);
@@ -391,6 +397,12 @@ lbool iz3interpolate(ast_manager &_m_manager,
   return res;
 }
 
+void interpolation_options_struct::apply(iz3base &b){
+  for(stl_ext::hash_map<std::string,std::string>::iterator it = map.begin(), en = map.end();
+      it != en;
+      ++it)
+    b.set_option((*it).first,(*it).second);
+}
 
 
 

src/interp/iz3interp.h

@@ -23,8 +23,15 @@ Revision History:
 #include "iz3hash.h"
 #include "solver.h"
 
+class iz3base;
+
 struct interpolation_options_struct {
   stl_ext::hash_map<std::string,std::string> map;
+public:
+  void set(const std::string &name, const std::string &value){
+    map[name] = value;
+  }
+  void apply(iz3base &b);
 };
 
 /** This object is thrown if a tree interpolation problem is mal-formed */

src/muz_qe/dl_context.cpp

@@ -1013,13 +1013,15 @@ namespace datalog {
     }
 
     lbool context::query(expr* query) {
-        new_query();
-        rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
-        rule_ref r(m_rule_manager);
-        for (; it != end; ++it) {
+        if(get_engine() != DUALITY_ENGINE) {
+          new_query();
+	  rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
+	  rule_ref r(m_rule_manager);
+	  for (; it != end; ++it) {
             r = *it;
             check_rule(r);
-        }        
+	  }     
+        }   
         switch(get_engine()) {
         case DATALOG_ENGINE:
             return rel_query(query);
@@ -1259,6 +1261,15 @@ namespace datalog {
         }
     }
    
+    void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names){
+        for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
+	  expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
+	  rules.push_back(r.get());
+	  //            rules.push_back(m_rule_fmls[i].get());
+	  names.push_back(m_rule_names[i]);
+        }
+    }
+
     void context::get_rules_as_formulas(expr_ref_vector& rules, svector<symbol>& names) {
         expr_ref fml(m);
         datalog::rule_manager& rm = get_rule_manager();

src/muz_qe/dl_context.h

@@ -238,6 +238,7 @@ namespace datalog {
         rule_set const & get_rules() { flush_add_rules(); return m_rule_set; }
 
         void get_rules_as_formulas(expr_ref_vector& fmls, svector<symbol>& names);
+        void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names);
 
         void add_fact(app * head);
         void add_fact(func_decl * pred, const relation_fact & fact);

src/muz_qe/duality_dl_interface.cpp

@@ -119,9 +119,9 @@ void dl_interface::check_reset() {
   m_ctx.ensure_opened();
 
   expr_ref_vector rules(m_ctx.get_manager());
-  svector< ::symbol> names;
-  
-  m_ctx.get_rules_as_formulas(rules, names);
+  svector< ::symbol> names;  
+  // m_ctx.get_rules_as_formulas(rules, names);
+   m_ctx.get_raw_rule_formulas(rules, names);
 
   // get all the rules as clauses
   std::vector<expr> &clauses = _d->clauses;
@@ -132,7 +132,7 @@ void dl_interface::check_reset() {
   }
   
   // turn the query into a clause
-  expr q(_d->ctx,query);
+  expr q(_d->ctx,m_ctx.bind_variables(query,false));
   
   std::vector<sort> b_sorts;
   std::vector<symbol> b_names;
@@ -146,7 +146,7 @@ void dl_interface::check_reset() {
   }
 
   expr qc = implies(q,_d->ctx.bool_val(false));
-  qc = _d->ctx.make_quant(Exists,b_sorts,b_names,qc);
+  qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc);
   clauses.push_back(qc);
   
   // get the background axioms