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;
// 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 ||
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 */
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() {
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:
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 );
}
}
}
}
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 "
// 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);
// 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
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()) {
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);
}
}
-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 );
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 );
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();
}
}
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:
/**
*/
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
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
if( inferArgTypes( n, typs, visited ) ){
return init( typs, n );
}else{
+ Trace("si-prt") << "Could not infer argument types." << std::endl;
return false;
}
}
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() );
}
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;
}
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] );
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;
d_conjuncts[0].push_back( cr );
}else{
d_conjuncts[1].push_back( cr );
+ if( ngroundSingleInvocation ){
+ d_conjuncts[3].push_back( cr );
+ }
}
}
}else{
}
}
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
}
}
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;
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() );
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;
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 );
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 );
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 );
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 );
};
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) {
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 );
+}
+
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 (){}
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) \
--- /dev/null
+; 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)
+
projects / cvc5.git / commitdiff