Extend synthesis solver to handle single invocation with additional universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.

1 files changed, 131 insertions, 131 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d37cbf12d..201585070 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1791,38 +1791,37 @@ void SmtEngine::setDefaults() {
     if( !options::cbqiPreRegInst.wasSetByUser()) {
       options::cbqiPreRegInst.set( true );
     }
-  }else{
-    //counterexample-guided instantiation for non-sygus
-    // enable if any quantifiers with arithmetic or datatypes
-    if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || 
-        options::cbqiAll() ){
-      if( !options::cbqi.wasSetByUser() ){
-        options::cbqi.set( true );
-      }
-    }
-    if( options::cbqiSplx() ){
-      //implies more general option
+  }
+  //counterexample-guided instantiation for non-sygus
+  // enable if any quantifiers with arithmetic or datatypes
+  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || 
+      options::cbqiAll() ){
+    if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
     }
-    if( options::cbqi() ){
-      //must rewrite divk
-      if( !options::rewriteDivk.wasSetByUser()) {
-        options::rewriteDivk.set( true );
-      }
+  }
+  if( options::cbqiSplx() ){
+    //implies more general option
+    options::cbqi.set( true );
+  }
+  if( options::cbqi() ){
+    //must rewrite divk
+    if( !options::rewriteDivk.wasSetByUser()) {
+      options::rewriteDivk.set( true );
     }
-    if( options::cbqi() && d_logic.isPure(THEORY_ARITH) ){
-      options::cbqiAll.set( false );
-      if( !options::quantConflictFind.wasSetByUser() ){
-        options::quantConflictFind.set( false );
-      }
-      if( !options::instNoEntail.wasSetByUser() ){
-        options::instNoEntail.set( false );
-      }
-      if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){
-        //only instantiation should happen at last call when model is avaiable
-        if( !options::instWhenMode.wasSetByUser() ){
-          options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
-        }
+  }
+  if( options::cbqi() && d_logic.isPure(THEORY_ARITH) ){
+    options::cbqiAll.set( false );
+    if( !options::quantConflictFind.wasSetByUser() ){
+      options::quantConflictFind.set( false );
+    }
+    if( !options::instNoEntail.wasSetByUser() ){
+      options::instNoEntail.set( false );
+    }
+    if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){
+      //only instantiation should happen at last call when model is avaiable
+      if( !options::instWhenMode.wasSetByUser() ){
+        options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
     }
   }
@@ -4252,13 +4251,22 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
 }
 
 Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
+  return checkSatisfiability( ex, inUnsatCore, false );
+}/* SmtEngine::checkSat() */
+
+Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
+  Assert(!ex.isNull());
+  return checkSatisfiability( ex, inUnsatCore, true );
+}/* SmtEngine::query() */
+
+Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQuery) {
   try {
     Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
     SmtScope smts(this);
     finalOptionsAreSet();
     doPendingPops();
 
-    Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
+    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << ex << ")" << endl;
 
     if(d_queryMade && !options::incrementalSolving()) {
       throw ModalException("Cannot make multiple queries unless "
@@ -4289,14 +4297,15 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
     // Add the formula
     if(!e.isNull()) {
       d_problemExtended = true;
+      Expr ea = isQuery ? e.notExpr() : e;
       if(d_assertionList != NULL) {
-        d_assertionList->push_back(e);
+        d_assertionList->push_back(ea);
       }
-      d_private->addFormula(e.getNode(), inUnsatCore);
+      d_private->addFormula(ea.getNode(), inUnsatCore);
     }
 
     Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-    r = check().asSatisfiabilityResult();
+    r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult();
 
     if (options::solveIntAsBV() > 0 &&r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
       r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
@@ -4307,7 +4316,11 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
     // Dump the query if requested
     if(Dump.isOn("benchmark")) {
       // the expr already got dumped out if assertion-dumping is on
-      Dump("benchmark") << CheckSatCommand(ex);
+      if( isQuery ){
+        Dump("benchmark") << QueryCommand(ex);
+      }else{
+        Dump("benchmark") << CheckSatCommand(ex);
+      }
     }
 
     // Pop the context
@@ -4318,7 +4331,7 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
 
     d_problemExtended = false;
 
-    Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
+    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << e << ") => " << r << endl;
 
     // Check that SAT results generate a model correctly.
     if(options::checkModels()) {
@@ -4349,98 +4362,85 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
       Result::RESOURCEOUT : Result::TIMEOUT;
     return Result(Result::SAT_UNKNOWN, why, d_filename);
   }
-}/* SmtEngine::checkSat() */
-
-Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
-  Assert(!ex.isNull());
-  Assert(ex.getExprManager() == d_exprManager);
-  SmtScope smts(this);
-  finalOptionsAreSet();
-  doPendingPops();
-  Trace("smt") << "SMT query(" << ex << ")" << endl;
-
-  try {
-    if(d_queryMade && !options::incrementalSolving()) {
-      throw ModalException("Cannot make multiple queries unless "
-                           "incremental solving is enabled "
-                           "(try --incremental)");
-    }
-
-    // Substitute out any abstract values in ex
-    Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-    // Ensure that the expression is type-checked at this point, and Boolean
-    ensureBoolean(e);
-
-    // check to see if a postsolve() is pending
-    if(d_needPostsolve) {
-      d_theoryEngine->postsolve();
-      d_needPostsolve = false;
-    }
-
-    // Push the context
-    internalPush();
-
-    // Note that a query has been made
-    d_queryMade = true;
-
-    // Add the formula
-    d_problemExtended = true;
-    if(d_assertionList != NULL) {
-      d_assertionList->push_back(e.notExpr());
-    }
-    d_private->addFormula(e.getNode().notNode(), inUnsatCore);
-
-    // Run the check
-    Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-    r = check().asValidityResult();
-    d_needPostsolve = true;
-
-    // Dump the query if requested
-    if(Dump.isOn("benchmark")) {
-      // the expr already got dumped out if assertion-dumping is on
-      Dump("benchmark") << QueryCommand(ex);
-    }
-
-    // Pop the context
-    internalPop();
-
-    // Remember the status
-    d_status = r;
-
-    d_problemExtended = false;
+}
 
-    Trace("smt") << "SMT query(" << e << ") ==> " << r << endl;
 
-    // Check that SAT results generate a model correctly.
-    if(options::checkModels()) {
-      if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
-         (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
-        checkModel(/* hard failure iff */ ! r.isUnknown());
+Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalException, LogicException) {
+  SmtScope smts(this);
+  Trace("smt") << "Check synth: " << e << std::endl;
+  Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
+  Expr e_check = e;
+  Node conj = Node::fromExpr( e );
+  Assert( conj.getKind()==kind::FORALL );
+  //possibly run quantifier elimination to make formula into single invocation
+  if( conj[1].getKind()==kind::EXISTS ){
+    Node conj_se = conj[1][1];
+    
+    Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
+    quantifiers::SingleInvocationPartition sip( kind::APPLY );
+    sip.init( conj_se );
+    Trace("smt-synth") << "...finished, got:" << std::endl;
+    sip.debugPrint("smt-synth");
+    
+    if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){
+      //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
+      //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), 
+      //  and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f.  We invoke synthesis solver on this result.
+    
+      //create new smt engine to do quantifier elimination
+      SmtEngine smt_qe( d_exprManager );
+      smt_qe.setLogic(getLogicInfo());
+      Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl;
+      //partition variables
+      std::vector< Node > qe_vars;
+      std::vector< Node > nqe_vars;
+      for( unsigned i=0; i<sip.d_all_vars.size(); i++ ){
+        Node v = sip.d_all_vars[i];
+        if( std::find( sip.d_si_vars.begin(), sip.d_si_vars.end(), v )==sip.d_si_vars.end() ){
+          qe_vars.push_back( v );
+        }else{
+          nqe_vars.push_back( v );
+        }
       }
-    }
-    // Check that UNSAT results generate a proof correctly.
-    if(options::checkProofs()) {
-      if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
-        TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
-        checkProof();
+      std::vector< Node > orig;
+      std::vector< Node > subs;
+      //skolemize non-qe variables
+      for( unsigned i=0; i<nqe_vars.size(); i++ ){
+        Node k = NodeManager::currentNM()->mkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" );
+        orig.push_back( nqe_vars[i] );
+        subs.push_back( k );
+        Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k << std::endl;
       }
-    }
-    // Check that UNSAT results generate an unsat core correctly.
-    if(options::checkUnsatCores()) {
-      if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
-        TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
-        checkUnsatCore();
+      for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){
+        orig.push_back( sip.d_func_inv[it->first] );
+        Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" );
+        subs.push_back( k );
+        Trace("smt-synth") << "  subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl;
       }
+      Node conj_se_ngsi = sip.getFullSpecification();
+      Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() );
+      Assert( !qe_vars.empty() );
+      conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs );
+      
+      Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl;
+      Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false );
+      Trace("smt-synth") << "Result : " << qe_res << std::endl;
+      
+      //create single invocation conjecture
+      Node qe_res_n = Node::fromExpr( qe_res );
+      qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() );
+      if( !nqe_vars.empty() ){
+        qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n );
+      }
+      Assert( conj.getNumChildren()==3 );
+      qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] );
+      Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl;
+      e_check = qe_res_n.toExpr();
     }
-
-    return r;
-  } catch (UnsafeInterruptException& e) {
-    AlwaysAssert(d_private->getResourceManager()->out());
-    Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ?
-      Result::RESOURCEOUT : Result::TIMEOUT;
-    return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
   }
-}/* SmtEngine::query() */
+  
+  return checkSatisfiability( e_check, true, false );
+}
 
 Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
   Assert(ex.getExprManager() == d_exprManager);
@@ -5059,10 +5059,10 @@ void SmtEngine::printSynthSolution( std::ostream& out ) {
   }
 }
 
-Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull) throw(TypeCheckingException, ModalException, LogicException) {
+Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) throw(TypeCheckingException, ModalException, LogicException) {
   SmtScope smts(this);
-  if(!d_logic.isPure(THEORY_ARITH)){
-    Warning() << "Unexpected logic for quantifier elimination." << endl;
+  if(!d_logic.isPure(THEORY_ARITH) && strict){
+    Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
   }
   Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
   Node n_e = Node::fromExpr( e );  
@@ -5081,11 +5081,16 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull) throw(TypeCh
   e_children.push_back( n_e[1] );
   e_children.push_back( n_attr );
   Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
-  Trace("smt-qe-debug") << "Query : " << nn_e << std::endl;
+  Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl;
   Assert( nn_e.getNumChildren()==3 );
-  Result r = query(nn_e.toExpr());
+  Result r = checkSatisfiability(nn_e.toExpr(), true, true);
   Trace("smt-qe") << "Query returned " << r << std::endl;
-  if(r.asSatisfiabilityResult().isSat() == Result::SAT || ( !doFull && r.asSatisfiabilityResult().isSat() != Result::UNSAT ) ) {
+  if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) {
+    if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){
+      stringstream ss;
+      ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
+      InternalError(ss.str().c_str());
+    }
     //get the instantiations for all quantified formulas
     std::map< Node, std::vector< Node > > insts;    
     d_theoryEngine->getInstantiations( insts );
@@ -5121,11 +5126,6 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull) throw(TypeCh
     ret_n = Rewriter::rewrite( ret_n.negate() );
     return ret_n.toExpr();
   }else {
-    if(r.asSatisfiabilityResult().isSat() != Result::UNSAT){
-      stringstream ss;
-      ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
-      InternalError(ss.str().c_str());
-    }
     return NodeManager::currentNM()->mkConst(true).toExpr();
   }
 }