Merge branch 'interp' of https://git01.codeplex.com/z3 into interp

src/duality/duality.h

@@ -174,6 +174,10 @@ namespace Duality {
 						    const std::vector<expr> &assumptions,
 						    const std::vector<expr> &theory
 						    ){}
+
+	   /** Cancel, throw Canceled object if possible. */
+	   virtual void cancel(){ }
+
 	   virtual ~LogicSolver(){}
       };
 
@@ -225,8 +229,11 @@ namespace Duality {
 #if 0
 	  islvr->write_interpolation_problem(file_name,assumptions,theory);
 #endif
+
 	}
 
+	void cancel(){islvr->cancel();}
+
 	/** Declare a constant in the background theory. */
 	virtual void declare_constant(const func_decl &f){
 	  bckg.insert(f);
@@ -835,6 +842,13 @@ namespace Duality {
 
       static Solver *Create(const std::string &solver_class, RPFP *rpfp);
 
+      /** This can be called asynchrnously to cause Solve to throw a
+	  Canceled exception at some time in the future.
+       */
+      virtual void Cancel() = 0;
 
+      /** Object thrown on cancellation */
+      struct Canceled {};
+      
     };
 }

src/duality/duality_solver.cpp

@@ -282,6 +282,10 @@ namespace Duality {
       return res;
     }
 
+    void Cancel(){
+      // TODO
+    }
+
 #if 0
     virtual void Restart(RPFP *_rpfp){
       rpfp = _rpfp;

src/duality/duality_wrapper.cpp

@@ -36,6 +36,7 @@ namespace Duality {
     p.set_bool("unsat_core", true); 
     scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
     m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
+    canceled = false;
   }
 
 expr context::constant(const std::string &name, const sort &ty){ 

src/duality/duality_wrapper.h

@@ -773,10 +773,11 @@ namespace Duality {
     protected:
         ::solver *m_solver;
         model the_model;
+	bool canceled;
     public:
         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(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;}
+        solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;}
         ~solver() {
 	  if(m_solver)
 	    dealloc(m_solver);
@@ -788,12 +789,18 @@ namespace Duality {
 	    the_model = s.the_model;
             return *this; 
         }
+	struct cancel_exception {};
+	void checkpoint(){
+	  if(canceled)
+	    throw(cancel_exception());
+	}
         // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
         void push() { m_solver->push(); }
         void pop(unsigned n = 1) { m_solver->pop(n); }
         // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
         void add(expr const & e) { m_solver->assert_expr(e); }
         check_result check() { 
+	  checkpoint();
 	  lbool r = m_solver->check_sat(0,0);
 	  model_ref m;
 	  m_solver->get_model(m);
@@ -808,6 +815,7 @@ namespace Duality {
 	  return res;
 	}
         check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) {
+	  checkpoint();
 	  std::vector< ::expr *> _assumptions(n);
 	  for (unsigned i = 0; i < n; i++) {
 	    _assumptions[i] = to_expr(assumptions[i]);
@@ -854,6 +862,11 @@ namespace Duality {
 	
 	int get_num_decisions(); 
 
+	void cancel(){
+	  canceled = true;
+	  if(m_solver)
+	    m_solver->cancel();
+	}
     };
 
 #if 0

src/muz_qe/dl_context.cpp

@@ -937,6 +937,7 @@ namespace datalog {
         if (m_bmc.get()) m_bmc->cancel();
         if (m_rel.get()) m_rel->cancel();
         if (m_tab.get()) m_tab->cancel();
+	if (m_duality.get()) m_duality->cancel();
     }
 
     void context::cleanup() {

src/muz_qe/duality_dl_interface.cpp

@@ -201,7 +201,13 @@ lbool dl_interface::query(::expr * query) {
   }
 
   // Solve!
-  bool ans = rs->Solve();
+  bool ans;
+  try {
+    ans = rs->Solve();
+  }
+  catch (Duality::solver::cancel_exception &exn){
+    throw default_exception("duality canceled");
+  }
   
   // profile!
 
@@ -361,6 +367,8 @@ expr_ref dl_interface::get_answer() {
 }
 
 void dl_interface::cancel() {
+  if(_d && _d->ls)
+    _d->ls->cancel();
 }
 
 void dl_interface::cleanup() {