From 346c85d145f6938ce7dce74e7e7cb855d5a6025a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 8 Mar 2016 12:10:41 -0600 Subject: [PATCH] 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. --- src/main/command_executor.cpp | 4 + src/main/command_executor_portfolio.cpp | 3 +- src/parser/smt2/Smt2.g | 4 +- src/smt/command.cpp | 53 ++++ src/smt/command.h | 18 ++ src/smt/smt_engine.cpp | 262 +++++++++--------- src/smt/smt_engine.h | 12 +- .../quantifiers/ce_guided_single_inv.cpp | 19 +- src/theory/quantifiers/ce_guided_single_inv.h | 9 +- .../quantifiers/quant_equality_engine.cpp | 139 +++++++--- .../quantifiers/quant_equality_engine.h | 9 + test/regress/regress0/sygus/Makefile.am | 3 +- test/regress/regress0/sygus/max2-univ.sy | 12 + 13 files changed, 369 insertions(+), 178 deletions(-) create mode 100644 test/regress/regress0/sygus/max2-univ.sy 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(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(cmd) != NULL || - dynamic_cast(cmd) != NULL) { + dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL) { mode = 1; } else if(dynamic_cast(cmd) != NULL || dynamic_cast(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; id_checkProofTime); - checkProof(); + std::vector< Node > orig; + std::vector< Node > subs; + //skolemize non-qe variables + for( unsigned i=0; imkSkolem( "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: /** @@ -493,6 +495,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 @@ -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& 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; jd_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& 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; imkNode( 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 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 (){} diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 32caa4989..2ca807662 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -47,7 +47,8 @@ TESTS = commutative.sy \ list-head-x.sy \ clock-inc-tuple.sy \ dt-test-ns.sy \ - no-mention.sy + no-mention.sy \ + max2-univ.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy new file mode 100644 index 000000000..3f8aac3b2 --- /dev/null +++ b/test/regress/regress0/sygus/max2-univ.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi --no-dump-synth +; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes) +(set-logic LIA) +(synth-fun max2 ((x Int) (y Int)) Int) +(declare-var x Int) +(declare-var y Int) +(declare-var r Int) +(declare-var w Int) +(constraint (=> (< r 0) (=> (or (and (= x w) (= y (+ w r))) (and (= x (+ w r)) (= y w))) (= (max2 x y) w)))) +(check-synth) + -- 2.30.2