integrating duality

src/duality/duality.h

@@ -171,6 +171,7 @@ namespace Duality {
 						    const std::vector<expr> &assumptions,
 						    const std::vector<expr> &theory
 						    ){}
+	   virtual ~LogicSolver(){}
       };
 
       /** This solver uses iZ3. */
@@ -205,8 +206,8 @@ namespace Duality {
         }
 #endif
 
-        iZ3LogicSolver(context c){
+        iZ3LogicSolver(context &c){
-          ctx = ictx = new interpolating_context(c);
+          ctx = ictx = &c;
           slvr = islvr = new interpolating_solver(*ictx);
           need_goals = false;
           islvr->SetWeakInterpolants(true);
@@ -221,7 +222,7 @@ namespace Duality {
 #endif
 	}
         ~iZ3LogicSolver(){
-          delete ictx;
+          // delete ictx;
           delete islvr;
         }
       };

src/duality/duality_rpfp.cpp

@@ -590,7 +590,12 @@ namespace Duality {
     if (res == l_false)
       {
 	DecodeTree(root, interpolant->getChildren()[0], persist);
+	delete interpolant;
       }
+
+    delete tree;
+    if(goals)
+      delete goals;
     
     timer_stop("Solve");
     return res;
@@ -828,6 +833,7 @@ namespace Duality {
     return res;
   }
 
+
 #ifdef Z3OPS
   static Z3_subterm_truth *stt;
 #endif

src/duality/duality_solver.cpp

@@ -267,6 +267,8 @@ namespace Duality {
       //  print_profile(std::cout);
       delete indset;
       delete heuristic;
+      delete unwinding;
+      delete reporter;
       return res;
     }
 
@@ -1284,6 +1286,8 @@ namespace Duality {
       DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); 
       bool res = dt.Derive(unwinding,node,UseUnderapprox,true); // build full tree
       if(!res) throw "Duality internal error in BuildFullCex";
+      if(cex.tree)
+	delete cex.tree;
       cex.tree = dt.tree;
       cex.root = dt.top;
     }

src/duality/duality_wrapper.cpp

@@ -161,6 +161,33 @@ expr context::make_quant(decl_kind op, const std::vector<expr> &bvs, const expr
   return cook(result.get());
 }
 
+expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const std::vector<symbol> &_names, const expr &body){
+  if(_sorts.size() == 0) return body;
+
+
+  std::vector< ::symbol> names;
+  std::vector< ::sort *> types;
+  std::vector< ::expr *>  bound_asts;
+  unsigned num_bound = _sorts.size();
+
+  for (unsigned i = 0; i < num_bound; ++i) {
+    names.push_back(_names[i]);
+    types.push_back(to_sort(_sorts[i].raw()));
+  }
+  expr_ref result(m());
+  result = m().mk_quantifier(
+			     op == Forall, 
+			     names.size(), &types[0], &names[0], to_expr(body.raw()),            
+			     0, 
+			     ::symbol(),
+			     ::symbol(),
+			     0, 0,
+			     0, 0
+			     );
+  return cook(result.get());
+}
+
+
   decl_kind func_decl::get_decl_kind() const {
     return ctx().get_decl_kind(*this);
   }
@@ -453,6 +480,10 @@ expr context::make_quant(decl_kind op, const std::vector<expr> &bvs, const expr
       for(unsigned i = 0; i < _interpolants.size(); i++)
 	linearized_interpolants[i] = expr(ctx(),_interpolants[i]);
 
+      // since iz3interpolant returns interpolants with one ref count, we decrement here
+      for(unsigned i = 0; i < _interpolants.size(); i++)
+	m().dec_ref(_interpolants[i]);
+
       unlinearize_interpolants(0,assumptions,linearized_interpolants,interpolant);
       interpolant->setTerm(ctx().bool_val(false));
     }

src/duality/duality_wrapper.h

@@ -234,6 +234,7 @@ namespace Duality {
       expr make(decl_kind op, const expr &arg0, const expr &arg1, const expr &arg2);
 
       expr make_quant(decl_kind op, const std::vector<expr> &bvs, const expr &body);
+      expr make_quant(decl_kind op, const std::vector<sort> &_sorts, const std::vector<symbol> &_names, const expr &body);
 
 
       decl_kind get_decl_kind(const func_decl &t);
@@ -771,7 +772,10 @@ namespace Duality {
         solver(context & c);
         solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; }
         solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver;}
-        ~solver() { }
+        ~solver() {
+	  if(m_solver)
+	    dealloc(m_solver);
+	}
 	operator ::solver*() const { return m_solver; }
         solver & operator=(solver const & s) {
             m_ctx = s.m_ctx; 
@@ -1202,6 +1206,11 @@ namespace Duality {
 	num = _num;
       }
 
+      ~TermTree(){
+	for(unsigned i = 0; i < children.size(); i++)
+	  delete children[i];
+      }
+
     private:
       expr term;
       std::vector<TermTree *> children;

src/muz_qe/dl_context.cpp

@@ -1186,7 +1186,9 @@ namespace datalog {
             m_tab->display_certificate(out);
             return true;
 	case DUALITY_ENGINE:
-	  return false;
+            ensure_duality();
+            m_duality->display_certificate(out);
+	    return true;
         default: 
             return false;
         }        

src/muz_qe/duality_dl_interface.cpp

@@ -0,0 +1,333 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    duality_dl_interface.cpp
+
+Abstract:
+
+    SMT2 interface for Duality
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-9-22.
+    Modified by Ken McMIllan (kenmcmil) 2013-4-18.
+
+Revision History:
+
+--*/
+
+#include "dl_cmds.h"
+#include "dl_context.h"
+#include "dl_mk_coi_filter.h"
+#include "dl_mk_interp_tail_simplifier.h"
+#include "dl_mk_subsumption_checker.h"
+#include "dl_mk_rule_inliner.h"
+#include "dl_rule.h"
+#include "dl_rule_transformer.h"
+#include "dl_mk_extract_quantifiers.h"
+#include "smt2parser.h"
+#include "duality_dl_interface.h"
+#include "dl_rule_set.h"
+#include "dl_mk_slice.h"
+#include "dl_mk_unfold.h"
+#include "dl_mk_coalesce.h"
+#include "expr_abstract.h"
+#include "model_smt2_pp.h"
+
+#include "duality.h"
+
+using namespace Duality;
+
+namespace Duality {
+
+  enum DualityStatus {StatusModel, StatusRefutation, StatusUnknown, StatusNull};
+
+  class duality_data {
+  public:
+    context ctx;
+    RPFP::LogicSolver *ls;
+    RPFP *rpfp;
+    
+    DualityStatus status;
+    std::vector<expr> clauses;
+    hash_map<RPFP::Edge *,int> map;  // edges to clauses
+    Solver::Counterexample cex;
+
+    duality_data(ast_manager &_m) : ctx(_m,config(params_ref())) {
+      ls = 0;
+      rpfp = 0;
+      status = StatusNull;
+    }
+    ~duality_data(){
+      if(rpfp)
+	dealloc(rpfp);
+      if(ls)
+	dealloc(ls);
+      if(cex.tree)
+	delete cex.tree;
+    }
+  };
+
+
+dl_interface::dl_interface(datalog::context& dl_ctx) :  m_ctx(dl_ctx)
+
+{
+  _d = alloc(duality_data,dl_ctx.get_manager());
+  _d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx);
+  _d->rpfp = alloc(RPFP,_d->ls);
+}
+
+
+dl_interface::~dl_interface() {
+  dealloc(_d);
+}
+
+
+//
+// Check if the new rules are weaker so that we can 
+// re-use existing context.
+// 
+#if 0
+void dl_interface::check_reset() {
+  // TODO
+    datalog::rule_ref_vector const& new_rules = m_ctx.get_rules().get_rules();
+    datalog::rule_ref_vector const& old_rules = m_old_rules.get_rules();  
+    bool is_subsumed = !old_rules.empty();
+    for (unsigned i = 0; is_subsumed && i < new_rules.size(); ++i) {
+        is_subsumed = false;
+        for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) {
+            if (m_ctx.check_subsumes(*old_rules[j], *new_rules[i])) {
+                is_subsumed = true;
+            }
+        }
+        if (!is_subsumed) {
+            TRACE("pdr", new_rules[i]->display(m_ctx, tout << "Fresh rule "););
+            m_context->reset();
+        }
+    }
+    m_old_rules.reset();
+    m_old_rules.add_rules(new_rules.size(), new_rules.c_ptr());
+}
+#endif
+
+
+  lbool dl_interface::query(::expr * query) {
+  // TODO: you can only call this once!
+  // we restore the initial state in the datalog context
+  m_ctx.ensure_opened();
+
+  expr_ref_vector rules(m_ctx.get_manager());
+  svector< ::symbol> names;
+  
+  m_ctx.get_rules_as_formulas(rules, names);
+
+  // get all the rules as clauses
+  std::vector<expr> &clauses = _d->clauses;
+  clauses.clear();
+  for (unsigned i = 0; i < rules.size(); ++i) {
+    expr e(_d->ctx,rules[i].get());
+    clauses.push_back(e);
+  }
+  
+  // turn the query into a clause
+  expr q(_d->ctx,query);
+  
+  std::vector<sort> b_sorts;
+  std::vector<symbol> b_names;
+  if (q.is_quantifier() && !q.is_quantifier_forall()) {
+    int bound = q.get_quantifier_num_bound();
+    for(int j = 0; j < bound; j++){
+      b_sorts.push_back(q.get_quantifier_bound_sort(j));
+      b_names.push_back(q.get_quantifier_bound_name(j));
+    }
+    q = q.arg(0);
+  }
+
+  expr qc = implies(q,_d->ctx.bool_val(false));
+  qc = _d->ctx.make_quant(Exists,b_sorts,b_names,qc);
+  clauses.push_back(qc);
+  
+  // get the background axioms
+  unsigned num_asserts = m_ctx.get_num_assertions();
+  for (unsigned i = 0; i < num_asserts; ++i) {
+    expr e(_d->ctx,m_ctx.get_assertion(i));
+    _d->rpfp->AssertAxiom(e);
+  }
+  
+  // creates 1-1 map between clauses and rpfp edges
+  _d->rpfp->FromClauses(clauses);
+
+  // populate the edge-to-clause map
+  for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i)
+    _d->map[_d->rpfp->edges[i]] = i;
+     
+  // create a solver object
+
+  Solver *rs = Solver::Create("duality", _d->rpfp);
+
+  // set its options
+  IF_VERBOSE(1, rs->SetOption("report","1"););
+  rs->SetOption("full_expand",m_ctx.get_params().full_expand() ? "1" : "0");
+  rs->SetOption("no_conj",m_ctx.get_params().no_conj() ? "1" : "0");
+  rs->SetOption("feasible_edges",m_ctx.get_params().feasible_edges() ? "1" : "0");
+  rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
+  rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
+  unsigned rb = m_ctx.get_params().recursion_bound();
+  if(rb != UINT_MAX){
+    std::ostringstream os; os << rb;
+    rs->SetOption("recursion_bound", os.str());
+  }
+
+  // Solve!
+  bool ans = rs->Solve();
+  
+  // save the result and counterexample if there is one
+  _d->status = ans ? StatusModel : StatusRefutation;
+  _d->cex = rs->GetCounterexample();
+  
+  dealloc(rs);
+
+  // true means the RPFP problem is SAT, so the query is UNSAT
+  return ans ? l_false : l_true;
+}
+
+expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
+    SASSERT(false);
+    return expr_ref(m_ctx.get_manager());
+}
+
+  void dl_interface::add_cover(int level, ::func_decl* pred, ::expr* property) {
+    SASSERT(false);
+}
+
+  unsigned dl_interface::get_num_levels(::func_decl* pred) {
+    SASSERT(false);
+    return 0;
+}
+
+  void dl_interface::collect_statistics(::statistics& st) const {
+}
+
+void dl_interface::reset_statistics() {
+}
+
+static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexample &cex) {
+  context &ctx = d->dd()->ctx;
+  RPFP::Node &node = *cex.root;
+  RPFP::Edge &edge = *node.Outgoing;
+  
+  // first, prove the children (that are actually used)
+
+  for(unsigned i = 0; i < edge.Children.size(); i++){
+    if(!cex.tree->Empty(edge.Children[i])){
+      Solver::Counterexample foo = cex;
+      foo.root = edge.Children[i];
+      print_proof(d,out,foo);
+    }
+  }
+
+  // print the label and the proved fact
+
+  out << "(" << node.number;
+  out << " (" << node.Name.name();
+  for(unsigned i = 0; i < edge.F.IndParams.size(); i++)
+    out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]);
+  out << ")\n";
+
+  // print the substitution
+
+  out << "  (\n";
+  RPFP::Edge *orig_edge = edge.map;
+  int orig_clause = d->dd()->map[orig_edge];
+  expr &t = d->dd()->clauses[orig_clause];
+  if (t.is_quantifier() && t.is_quantifier_forall()) {
+    int bound = t.get_quantifier_num_bound();
+    std::vector<sort> sorts;
+    std::vector<symbol> names;
+    hash_map<int,expr> subst;
+    for(int j = 0; j < bound; j++){
+      sort the_sort = t.get_quantifier_bound_sort(j);
+      symbol name = t.get_quantifier_bound_name(j);
+      expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
+      out << "    (= " << skolem << " " << cex.tree->Eval(&edge,skolem) << ")\n";
+    }
+  }
+  out << "  )\n";
+  
+  // reference the proofs of all the children, in syntactic order
+  // "true" means the child is not needed
+  
+  out << "  (";
+  for(unsigned i = 0; i < edge.Children.size(); i++){
+    if(!cex.tree->Empty(edge.Children[i]))
+      out << " " << edge.Children[i]->number;
+    else
+      out << " true";
+  }
+  out << "  )";
+  out << ")\n";
+}
+
+
+void dl_interface::display_certificate(std::ostream& out) {
+  if(_d->status == StatusModel){
+    ast_manager &m = m_ctx.get_manager();
+    model_ref md = get_model();
+    model_smt2_pp(out, m, *md.get(), 0); 
+  }
+  else if(_d->status == StatusRefutation){
+    out << "(\n";
+    // negation of the query is the last clause -- prove it
+    print_proof(this,out,_d->cex);
+    out << ")\n";
+  }
+}
+
+expr_ref dl_interface::get_answer() {
+    SASSERT(false);
+    return expr_ref(m_ctx.get_manager());
+}
+
+void dl_interface::cancel() {
+}
+
+void dl_interface::cleanup() {
+}
+
+void dl_interface::updt_params() {
+}
+
+model_ref dl_interface::get_model() {
+  ast_manager &m = m_ctx.get_manager();
+  model_ref md(alloc(::model, m));
+  std::vector<RPFP::Node *> &nodes = _d->rpfp->nodes;
+  expr_ref_vector conjs(m);
+  for (unsigned i = 0; i < nodes.size(); ++i) {
+    RPFP::Node *node = nodes[i];
+    func_decl &pred = node->Name;
+    expr_ref prop(m);
+    prop = to_expr(node->Annotation.Formula);
+    std::vector<expr> &params = node->Annotation.IndParams;
+    expr_ref q(m);
+    expr_ref_vector sig_vars(m);
+    for (unsigned j = 0; j < params.size(); ++j)
+      sig_vars.push_back(params[params.size()-j-1]); // TODO: why backwards?
+    expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q);
+    if (params.empty()) {
+      md->register_decl(pred, q);
+    }
+    else {
+      ::func_interp* fi = alloc(::func_interp, m, params.size());
+      fi->set_else(q);
+      md->register_decl(pred, fi);
+    }
+  }
+  return md;
+}
+  
+proof_ref dl_interface::get_proof() {
+  return proof_ref(m_ctx.get_manager());
+}
+}

src/muz_qe/duality_dl_interface.h

@@ -0,0 +1,76 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    duality_dl_interface.h
+
+Abstract:
+
+    SMT2 interface for Duality
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-9-22.
+    Modified by Ken McMIllan (kenmcmil) 2013-4-18.
+
+Revision History:
+
+--*/
+
+#ifndef _DUALITY_DL_INTERFACE_H_
+#define _DUALITY_DL_INTERFACE_H_
+
+#include "lbool.h"
+#include "dl_rule.h"
+#include "dl_rule_set.h"
+#include "statistics.h"
+
+namespace datalog {
+    class context;
+}
+
+namespace Duality {
+
+    class duality_data;
+
+    class dl_interface {
+        duality_data *_d;
+	datalog::context &m_ctx;
+
+    public:
+        dl_interface(datalog::context& ctx); 
+        ~dl_interface();
+        
+        lbool query(expr* query);
+
+        void cancel();
+
+        void cleanup();
+
+        void display_certificate(std::ostream& out);
+
+        void collect_statistics(statistics& st) const;
+
+        void reset_statistics();
+
+        expr_ref get_answer();
+
+        unsigned get_num_levels(func_decl* pred);
+
+        expr_ref get_cover_delta(int level, func_decl* pred);
+       
+        void add_cover(int level, func_decl* pred, expr* property);
+               
+        void updt_params();
+
+        model_ref get_model();
+
+        proof_ref get_proof();
+        
+	duality_data *dd(){return _d;}
+    };
+}
+
+
+#endif

src/muz_qe/fixedpoint_params.pyg

@@ -58,6 +58,12 @@ def_module_params('fixedpoint',
                           ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'),
                           ('print_statistics',  BOOL, False, 'print statistics'),
 	                  ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'),
+	                  ('full_expand', BOOL, False, 'DUALITY: Fully expand derivation trees'),
+	                  ('no_conj', BOOL, False, 'DUALITY: No forced covering (conjectures)'),
+	                  ('feasible_edges', BOOL, True, 'DUALITY: Don\'t expand definitley infeasible edges'),
+	                  ('use_underapprox', BOOL, False, 'DUALITY: Use underapproximations'),
+			  ('stratified_inlining', BOOL, False, 'DUALITY: Use stratified inlining'),
+			  ('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'),
                           ))