fussing with qe in duality

scripts/mk_project.py

@@ -55,8 +55,8 @@ def init_project_def():
     add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
-    add_lib('duality', ['smt', 'interp'])
     add_lib('qe', ['smt','sat'], 'qe')
+    add_lib('duality', ['smt', 'interp', 'qe'])
     add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base')
     add_lib('transforms', ['muz', 'hilbert'], 'muz/transforms')
     add_lib('rel', ['muz', 'transforms'], 'muz/rel')

src/duality/duality.h

@@ -97,7 +97,8 @@ namespace Duality {
 
       bool IsClosedFormula(const Term &t);
 
-  private:
+      Term AdjustQuantifiers(const Term &t);
+private:
 
       void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
       int CountOperatorsRec(hash_set<ast> &memo, const Term &t);

src/duality/duality_rpfp.cpp

@@ -573,6 +573,13 @@ namespace Duality {
     return RemoveRedundancyRec(memo,smemo,t);
   }
 
+  Z3User::Term Z3User::AdjustQuantifiers(const Term &t)
+  {
+    if(t.is_quantifier() || (t.is_app() && t.has_quantifiers()))
+      return t.qe_lite();
+    return t;
+  }
+
   Z3User::Term Z3User::SubstRecHide(hash_map<ast, Term> &memo, const Term &t, int number)
   {
     std::pair<ast,Term> foo(t,expr(ctx));
@@ -2136,6 +2143,7 @@ namespace Duality {
     g = RemoveRedundancy(g);
     g = g.simplify();
 #endif
+    g = AdjustQuantifiers(g);
     return g;
   }
 

src/duality/duality_solver.cpp

@@ -1819,7 +1819,7 @@ namespace Duality {
       }
       
       bool NodeTooComplicated(Node *node){
-	return tree->CountOperators(node->Annotation.Formula) > 5;
+	return tree->CountOperators(node->Annotation.Formula) > 3;
       }
 
       void SimplifyNode(Node *node){

src/duality/duality_wrapper.cpp

@@ -26,6 +26,7 @@ Revision History:
 #include "expr_abstract.h"
 #include "stopwatch.h"
 #include "model_smt2_pp.h"
+#include "qe_lite.h"
 
 namespace Duality {
 
@@ -329,6 +330,14 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return simplify(p);
   }
 
+  expr expr::qe_lite() const {
+    ::qe_lite qe(m());
+    expr_ref result(to_expr(raw()),m());
+    proof_ref pf(m());
+    qe(result,pf);
+    return ctx().cook(result);
+  }
+
   expr clone_quantifier(const expr &q, const expr &b){
     return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
   }

src/duality/duality_wrapper.h

@@ -558,6 +558,8 @@ namespace Duality {
 
         expr simplify(params const & p) const;
 	
+        expr qe_lite() const;
+
 	friend expr clone_quantifier(const expr &, const expr &);
 
         friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);