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.

11 files changed, 355 insertions, 177 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 672dedc50..cfd0f708c 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -115,6 +115,10 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if(q != NULL) {
     d_result = res = q->getResult();
   }
+  CheckSynthCommand* csy = dynamic_cast<CheckSynthCommand*>(cmd);
+  if(csy != NULL) {
+    d_result = res = csy->getResult();
+  }
 
   if((cs != NULL || q != NULL) && d_options.getStatsEveryQuery()) {
     std::ostringstream ossCurStats;
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 15165e82c..6832c5912 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -198,7 +198,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
   // command
 
   if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
-     dynamic_cast<QueryCommand*>(cmd) != NULL) {
+     dynamic_cast<QueryCommand*>(cmd) != NULL ||
+     dynamic_cast<CheckSynthCommand*>(cmd) != NULL) {
     mode = 1;
   } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
             dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9d2392715..0526ba66d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -765,9 +765,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       Command* c = new SetUserAttributeCommand("sygus", sygusVar);
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
-      c = new AssertCommand(body);
-      PARSER_STATE->preemptCommand(c);
-      $cmd = new CheckSatCommand();
+      $cmd = new CheckSynthCommand(body);
     }
   | c = command { $cmd = c; }
  //   /* error handling */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 89d7b5ca2..5bf74a7de 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -376,6 +376,59 @@ std::string QueryCommand::getCommandName() const throw() {
   return "query";
 }
 
+
+/* class CheckSynthCommand */
+
+CheckSynthCommand::CheckSynthCommand() throw() :
+  d_expr() {
+}
+
+CheckSynthCommand::CheckSynthCommand(const Expr& expr, bool inUnsatCore) throw() :
+  d_expr(expr), d_inUnsatCore(inUnsatCore) {
+}
+
+Expr CheckSynthCommand::getExpr() const throw() {
+  return d_expr;
+}
+
+void CheckSynthCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->checkSynth(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Result CheckSynthCommand::getResult() const throw() {
+  return d_result;
+}
+
+void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out, verbosity);
+  } else {
+    out << d_result << endl;
+  }
+}
+
+Command* CheckSynthCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+  c->d_result = d_result;
+  return c;
+}
+
+Command* CheckSynthCommand::clone() const {
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr, d_inUnsatCore);
+  c->d_result = d_result;
+  return c;
+}
+
+std::string CheckSynthCommand::getCommandName() const throw() {
+  return "check-synth";
+}
+
+
 /* class ResetCommand */
 
 void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
diff --git a/src/smt/command.h b/src/smt/command.h
index 512f147da..7c9706522 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -501,6 +501,24 @@ public:
   std::string getCommandName() const throw();
 };/* class QueryCommand */
 
+class CVC4_PUBLIC CheckSynthCommand : public Command {
+protected:
+  Expr d_expr;
+  Result d_result;
+  bool d_inUnsatCore;
+public:
+  CheckSynthCommand() throw();
+  CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw();
+  ~CheckSynthCommand() throw() {}
+  Expr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Result getResult() const throw();
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+  std::string getCommandName() const throw();
+};/* class CheckSynthCommand */
+
 // this is TRANSFORM in the CVC presentation language
 class CVC4_PUBLIC SimplifyCommand : public Command {
 protected:
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();
   }
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 68ea9c595..74ff0edb3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -401,6 +401,8 @@ class CVC4_PUBLIC SmtEngine {
   SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
   SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
 
+  //check satisfiability (for query and check-sat)
+  Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery);
 public:
 
   /**
@@ -494,6 +496,12 @@ public:
   Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
 
   /**
+   * Assert a synthesis conjecture to the current context and call
+   * check().  Returns sat, unsat, or unknown result.
+   */
+  Result checkSynth(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
+
+  /**
    * Simplify a formula without doing "much" work.  Does not involve
    * the SAT Engine in the simplification, but uses the current
    * definitions, assertions, and the current partial model, if one
@@ -553,9 +561,9 @@ public:
   void printSynthSolution( std::ostream& out );
 
   /**
-   * Do quantifier elimination, doFull false means just output one disjunct
+   * Do quantifier elimination, doFull false means just output one disjunct, strict is whether to output warnings.
    */
-  Expr doQuantifierElimination(const Expr& e, bool doFull) throw(TypeCheckingException, ModalException, LogicException);
+  Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException);
 
   /**
    * Get an unsatisfiable core (only if immediately preceded by an
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 80585a33d..850c98437 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -845,6 +845,7 @@ bool SingleInvocationPartition::init( Node n ) {
   if( inferArgTypes( n, typs, visited ) ){
     return init( typs, n );  
   }else{
+    Trace("si-prt") << "Could not infer argument types." << std::endl;
     return false;
   }
 }
@@ -854,7 +855,7 @@ bool SingleInvocationPartition::inferArgTypes( Node n, std::vector< TypeNode >&
     visited[n] = true;
     if( n.getKind()!=FORALL ){
     //if( TermDb::hasBoundVarAttr( n ) ){
-      if( n.getKind()==APPLY_UF ){
+      if( n.getKind()==d_checkKind ){
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           typs.push_back( n[i].getType() );
         }
@@ -882,6 +883,7 @@ bool SingleInvocationPartition::init( std::vector< TypeNode >& typs, Node n ){
     Node si_v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_arg_types[j] );
     d_si_vars.push_back( si_v );
   }
+  Trace("si-prt") << "Process the formula..." << std::endl;
   process( n );
   return true;
 }
@@ -909,6 +911,7 @@ void SingleInvocationPartition::process( Node n ) {
       std::vector< Node > terms;
       std::vector< Node > subs;
       bool singleInvocation = true;
+      bool ngroundSingleInvocation = false;
       if( processConjunct( cr, visited, args, terms, subs ) ){
         for( unsigned j=0; j<terms.size(); j++ ){
           si_terms.push_back( subs[j] );
@@ -944,6 +947,7 @@ void SingleInvocationPartition::process( Node n ) {
         TermDb::getBoundVars( cr, bvs );
         if( bvs.size()>d_si_vars.size() ){
           Trace("si-prt") << "...not ground single invocation." << std::endl;
+          ngroundSingleInvocation = true;
           singleInvocation = false;
         }else{
           Trace("si-prt") << "...ground single invocation : success." << std::endl;
@@ -984,6 +988,9 @@ void SingleInvocationPartition::process( Node n ) {
         d_conjuncts[0].push_back( cr );
       }else{
         d_conjuncts[1].push_back( cr );
+        if( ngroundSingleInvocation ){
+          d_conjuncts[3].push_back( cr );
+        }
       }
     }
   }else{
@@ -1026,7 +1033,7 @@ bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >&
         }
       }
       if( ret ){
-        if( n.getKind()==APPLY_UF ){
+        if( n.getKind()==d_checkKind ){
           if( std::find( terms.begin(), terms.end(), n )==terms.end() ){
             Node f = n.getOperator();
             //check if it matches the type requirement
@@ -1083,7 +1090,7 @@ bool SingleInvocationPartition::isAntiSkolemizableType( Node f ) {
         }
       }
       if( ret ){
-        Node t = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+        Node t = NodeManager::currentNM()->mkNode( d_checkKind, children );
         d_func_inv[f] = t;
         d_inv_to_func[t] = f;
         std::stringstream ss;
@@ -1117,7 +1124,7 @@ Node SingleInvocationPartition::getSpecificationInst( Node n, std::map< Node, No
       childChanged = childChanged || ( nn!=n[i] );
     }
     Node ret;
-    if( n.getKind()==APPLY_UF ){
+    if( n.getKind()==d_checkKind ){
       std::map< Node, Node >::iterator itl = lam.find( n.getOperator() );
       if( itl!=lam.end() ){
         Assert( itl->second[0].getNumChildren()==children.size() );
@@ -1214,8 +1221,8 @@ void SingleInvocationPartition::debugPrint( const char * c ) {
       Trace(c) << "not incorporated." << std::endl;
     }
   }
-  for( unsigned i=0; i<3; i++ ){
-    Trace(c) << ( i==0 ? "Single invocation" : ( i==1 ? "Non-single invocation" : "All" ) );
+  for( unsigned i=0; i<4; i++ ){
+    Trace(c) << ( i==0 ? "Single invocation" : ( i==1 ? "Non-single invocation" : ( i==2 ? "All" : "Non-ground single invocation" ) ) );
     Trace(c) << " conjuncts: " << std::endl;
     for( unsigned j=0; j<d_conjuncts[i].size(); j++ ){
       Trace(c) << "  " << (j+1) << " : " << d_conjuncts[i][j] << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index fe48a0dc3..c25cf7633 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -153,6 +153,8 @@ public:
 class SingleInvocationPartition
 {
 private:
+  //options
+  Kind d_checkKind;
   bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited );
   void process( Node n );
   bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj );
@@ -161,6 +163,8 @@ private:
   Node getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited );
   void extractInvariant2( Node n, Node& func, int& pol, std::vector< Node >& disjuncts, bool hasPol, std::map< Node, bool >& visited );
 public:
+  SingleInvocationPartition( Kind checkKind = kind::APPLY_UF ) : d_checkKind( checkKind ){}
+  ~SingleInvocationPartition(){}
   bool init( Node n );
   bool init( std::vector< TypeNode >& typs, Node n );
 
@@ -174,8 +178,8 @@ public:
   std::vector< Node > d_func_vars; //the first-order variables corresponding to all functions
   std::vector< Node > d_si_vars;   //the arguments that we based the anti-skolemization on
   std::vector< Node > d_all_vars;  //every free variable of conjuncts[2]
-  // si, nsi, all
-  std::vector< Node > d_conjuncts[3];
+  // si, nsi, all, non-ground si
+  std::vector< Node > d_conjuncts[4];
 
   bool isAntiSkolemizableType( Node f );
 
@@ -189,6 +193,7 @@ public:
   void extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts );
 
   bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
+  bool isNonGroundSingleInvocation() { return d_conjuncts[3].size()==d_conjuncts[1].size(); }
 
   void debugPrint( const char * c );
 };
diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
index 54a931196..06ca6f98c 100644
--- a/src/theory/quantifiers/quant_equality_engine.cpp
+++ b/src/theory/quantifiers/quant_equality_engine.cpp
@@ -32,6 +32,7 @@ d_conflict(c, false),
 d_quant_red(c),
 d_quant_unproc(c){
   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
+  d_intType = NodeManager::currentNM()->integerType();
 }
 
 void QuantEqualityEngine::conflict(TNode t1, TNode t2) {
@@ -86,56 +87,130 @@ void QuantEqualityEngine::registerQuantifier( Node q ) {
 void QuantEqualityEngine::assertNode( Node n ) {
   Assert( n.getKind()==FORALL );
   Trace("qee-debug") << "QEE assert : " << n << std::endl;
-  Node lit = n[1].getKind()==NOT ? n[1][0] : n[1];
-  bool pol = n[1].getKind()!=NOT;
-  if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
-    lit = getTermDatabase()->getCanonicalTerm( lit );
-    Trace("qee-debug") << "Canonical :  " << lit << ", pol = " << pol << std::endl;
-    Node t1 = lit.getKind()==APPLY_UF ? lit : lit[0];
+  if( !d_conflict ){
+    Node lit = n[1].getKind()==NOT ? n[1][0] : n[1];
+    bool pol = n[1].getKind()!=NOT;
+    bool success = true;
+    Node t1;
     Node t2;
-    if( lit.getKind()==APPLY_UF ){
-      t2 = pol ? getTermDatabase()->d_true : getTermDatabase()->d_false;
-      pol = true;
+    if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL || lit.getKind()==IFF ){
+      lit = getTermDatabase()->getCanonicalTerm( lit );
+      Trace("qee-debug") << "Canonical :  " << lit << ", pol = " << pol << std::endl;
+      if( lit.getKind()==APPLY_UF ){
+        t1 = getFunctionAppForPredicateApp( lit );
+        t2 = pol ? getTermDatabase()->d_one : getTermDatabase()->d_zero;
+        pol = true;
+        lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
+      }else if( lit.getKind()==EQUAL ){
+        t1 = lit[0];
+        t2 = lit[1];
+      }else if( lit.getKind()==IFF ){
+        if( lit[0].getKind()==NOT ){
+          t1 = lit[0][0];
+          pol = !pol;
+        }else{
+          t1 = lit[0];
+        }
+        if( lit[1].getKind()==NOT ){
+          t2 = lit[1][0];
+          pol = !pol;
+        }else{
+          t2 = lit[1];
+        }
+        if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){
+          t1 = getFunctionAppForPredicateApp( t1 );
+          t2 = getFunctionAppForPredicateApp( t2 );
+          lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
+        }else{
+          success = false;
+        }
+      }
     }else{
-      t2 = lit[1];
-    }
-    bool alreadyHolds = false;
-    if( pol && areUnivEqual( t1, t2 ) ){
-      alreadyHolds = true;
-    }else if( !pol && areUnivDisequal( t1, t2 ) ){
-      alreadyHolds = true;
+      success = false;
     }
+    if( success ){
+      bool alreadyHolds = false;
+      if( pol && areUnivEqualInternal( t1, t2 ) ){
+        alreadyHolds = true;
+      }else if( !pol && areUnivDisequalInternal( t1, t2 ) ){
+        alreadyHolds = true;
+      }
 
-    if( alreadyHolds ){
-      d_quant_red.push_back( n );
-      Trace("qee-debug") << "...add to redundant" << std::endl;
-    }else{
-      Trace("qee-debug") << "...assert" << std::endl;
-      Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl;
-      if( lit.getKind()==APPLY_UF ){
-        d_uequalityEngine.assertPredicate(lit, pol, n);
+      if( alreadyHolds ){
+        d_quant_red.push_back( n );
+        Trace("qee-debug") << "...add to redundant" << std::endl;
       }else{
-        d_uequalityEngine.assertEquality(lit, pol, n);
+        Trace("qee-debug") << "...assert" << std::endl;
+        Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl;
+        if( lit.getKind()==APPLY_UF ){
+          d_uequalityEngine.assertPredicate(lit, pol, n);
+        }else{
+          d_uequalityEngine.assertEquality(lit, pol, n);
+        }
       }
+    }else{
+      d_quant_unproc[n] = true;
+      Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
     }
-  }else{
-    d_quant_unproc[n] = true;
-    Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
   }
 }
 
-bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) {
+bool QuantEqualityEngine::areUnivDisequalInternal( TNode n1, TNode n2 ) {
   return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
 }
 
-bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) {
+bool QuantEqualityEngine::areUnivEqualInternal( TNode n1, TNode n2 ) {
   return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
 }
 
-TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) {
+TNode QuantEqualityEngine::getUnivRepresentativeInternal( TNode n ) {
   if( d_uequalityEngine.hasTerm( n ) ){
     return d_uequalityEngine.getRepresentative( n );
   }else{
     return n;
   }
-}
\ No newline at end of file
+}
+bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) {
+  //TODO: must convert to internal representation
+  return areUnivDisequalInternal( n1, n2 );
+}
+
+bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) {
+  //TODO: must convert to internal representation
+  return areUnivEqualInternal( n1, n2 );
+}
+
+TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) {
+  //TODO: must convert to internal representation
+  return getUnivRepresentativeInternal( n );
+}
+
+Node QuantEqualityEngine::getFunctionForPredicate( Node f ) {
+  std::map< Node, Node >::iterator it = d_pred_to_func.find( f );
+  if( it==d_pred_to_func.end() ){
+    std::vector< TypeNode > argTypes;
+    TypeNode tn = f.getType();
+    for( unsigned i=0; i<(tn.getNumChildren()-1); i++ ){
+      argTypes.push_back( tn[i] );
+    }
+    TypeNode ftn = NodeManager::currentNM()->mkFunctionType( argTypes, d_intType  );
+    std::stringstream ss;
+    ss << "ee_" << f;
+    Node op = NodeManager::currentNM()->mkSkolem( ss.str(), ftn, "op created for internal ee" );
+    d_pred_to_func[f] = op;
+    return op;
+  }else{
+    return it->second;
+  }
+}
+
+Node QuantEqualityEngine::getFunctionAppForPredicateApp( Node n ) {
+  Assert( n.getKind()==APPLY_UF );
+  std::vector< Node > children;
+  children.push_back( getFunctionForPredicate( n.getOperator() ) );
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    children.push_back( n[i] );
+  }
+  return NodeManager::currentNM()->mkNode( APPLY_UF, children );
+}
+
diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
index 35a328147..f3d8db8aa 100644
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -56,12 +56,21 @@ private:
   context::CDList<Node> d_quant_red;
   /** unprocessed quantifiers in current context */
   NodeBoolMap d_quant_unproc;
+  // map predicates to functions over int
+  TypeNode d_intType;
+  std::map< Node, Node > d_pred_to_func;
+  Node getFunctionForPredicate( Node f );
+  Node getFunctionAppForPredicateApp( Node n );
 private:
   void conflict(TNode t1, TNode t2);
   void eqNotifyNewClass(TNode t);
   void eqNotifyPreMerge(TNode t1, TNode t2);
   void eqNotifyPostMerge(TNode t1, TNode t2);
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+  //queries
+  bool areUnivDisequalInternal( TNode n1, TNode n2 );
+  bool areUnivEqualInternal( TNode n1, TNode n2 );  
+  TNode getUnivRepresentativeInternal( TNode n );
 public:
   QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
   virtual ~QuantEqualityEngine() throw (){}