From: ajreynol Date: Tue, 20 Jan 2015 09:23:08 +0000 (+0100) Subject: Handle miniscoping of conjunctions in synthesis properties. Refactor construction... X-Git-Tag: cvc5-1.0.0~6435 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9e5b1fd1083c1c82d5bbc61a4a316211db629c43;p=cvc5.git Handle miniscoping of conjunctions in synthesis properties. Refactor construction of sygus datatypes. Expand define-fun in evaluators. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 920803c28..d2f38cc82 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -493,6 +493,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] CommandSequence* seq; std::vector datatypes; std::vector< std::vector > ops; + std::vector< std::vector< std::string > > cnames; + std::vector< std::vector< std::vector< CVC4::Type > > > cargs; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -599,6 +601,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] sorts.push_back(t); datatypes.push_back(Datatype(dname)); ops.push_back(std::vector()); + cnames.push_back(std::vector()); + cargs.push_back(std::vector >()); if(!PARSER_STATE->isUnresolvedType(dname)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); @@ -606,9 +610,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } // Note the official spec for NTDef is missing the ( parens ) // but they are necessary to parse SyGuS examples - LPAREN_TOK sygusGTerm[fun, datatypes.back(), ops.back()]+ RPAREN_TOK + LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back()]+ RPAREN_TOK RPAREN_TOK - { PARSER_STATE->popScope(); } + { PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() ); + PARSER_STATE->popScope(); } )+ RPAREN_TOK { PARSER_STATE->popScope(); @@ -691,7 +696,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] // SyGuS grammar term // fun is the name of the synth-fun this grammar term is for -sygusGTerm[std::string& fun, CVC4::Datatype& dt, std::vector& ops] +sygusGTerm[std::string& fun, std::vector& ops, std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs] @declarations { std::string name; Kind k; @@ -702,24 +707,24 @@ sygusGTerm[std::string& fun, CVC4::Datatype& dt, std::vector& ops] } : LPAREN_TOK ( builtinOp[k] - { ops.push_back(EXPR_MANAGER->operatorOf(k)); + { Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; + ops.push_back(EXPR_MANAGER->operatorOf(k)); name = kind::kindToString(k); - Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; } | symbol[name,CHECK_NONE,SYM_VARIABLE] { // what is this sygus term trying to accomplish here, if the // symbol isn't yet declared?! probably the following line will // fail, but we need an operator to continue here.. - Expr bv = PARSER_STATE->getVariable(name); - ops.push_back(bv); - Debug("parser-sygus") << "Sygus grammar " << fun << " : op : " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar " << fun; + Debug("parser-sygus") << " : op (declare=" << PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl; + if( !PARSER_STATE->isDefinedFunction(name) ){ + PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); + } + ops.push_back( PARSER_STATE->getVariable(name) ); } ) - { name = dt.getName() + "_" + name; - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - ctor = new CVC4::DatatypeConstructor(name, testerId); + { cnames.push_back( name ); + cargs.push_back( std::vector< CVC4::Type >() ); } ( //sortSymbol[t,CHECK_NONE] symbol[sname,CHECK_NONE,SYM_VARIABLE] @@ -727,75 +732,46 @@ sygusGTerm[std::string& fun, CVC4::Datatype& dt, std::vector& ops] ss << fun << "_" << sname; sname = ss.str(); if( PARSER_STATE->isDeclared(sname, SYM_SORT) ) { - t = PARSER_STATE->getSort(sname); + t = PARSER_STATE->getSort(sname); } else { - t = PARSER_STATE->mkUnresolvedType(sname); + t = PARSER_STATE->mkUnresolvedType(sname); } - std::stringstream cname; - cname << fun << "_" << name << "_" << ++count; - ctor->addArg(cname.str(), t); + cargs.back().push_back(t); } )+ RPAREN_TOK - { dt.addConstructor(*ctor); - delete ctor; } | INTEGER_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl; ops.push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)))); - name = dt.getName() + "_" + AntlrInput::tokenText($INTEGER_LITERAL); - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( AntlrInput::tokenText($INTEGER_LITERAL) ); + cargs.push_back( std::vector< CVC4::Type >() ); } | HEX_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal " << AntlrInput::tokenText($HEX_LITERAL) << std::endl; assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); ops.push_back(MK_CONST( BitVector(hexString, 16) )); - name = dt.getName() + "_" + AntlrInput::tokenText($HEX_LITERAL); - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( AntlrInput::tokenText($HEX_LITERAL) ); + cargs.push_back( std::vector< CVC4::Type >() ); } | BINARY_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal " << AntlrInput::tokenText($BINARY_LITERAL) << std::endl; assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); ops.push_back(MK_CONST( BitVector(binString, 2) )); - name = dt.getName() + "_" + AntlrInput::tokenText($BINARY_LITERAL); - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( AntlrInput::tokenText($BINARY_LITERAL) ); + cargs.push_back( std::vector< CVC4::Type >() ); } | symbol[name,CHECK_NONE,SYM_VARIABLE] { if( name[0] == '-' ){ //hack for unary minus Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl; ops.push_back(MK_CONST(Rational(name))); - name = dt.getName() + "_" + name; - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( name ); + cargs.push_back( std::vector< CVC4::Type >() ); }else{ Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl; Expr bv = PARSER_STATE->getVariable(name); ops.push_back(bv); - name = dt.getName() + "_" + name; - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( name ); + cargs.push_back( std::vector< CVC4::Type >() ); } } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d20d48b13..077f385b0 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -504,7 +504,7 @@ void Smt2::includeFile(const std::string& filename) { //Type t = getExprManager()->mkFunctionType(types, rangeType); //Debug("parser-sygus") << "...function type : " << t << std::endl; - + Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED); Debug("parser-sygus") << "...made function : " << lambda << std::endl; std::vector applyv; @@ -524,10 +524,30 @@ void Smt2::includeFile(const std::string& filename) { } } +void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, + std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) { + //minimize grammar goes here + + for( unsigned i=0; i& datatypeTypes, std::vector< std::vector >& ops, - std::map& evals, std::vector& terms, +Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vector< std::vector >& ops, + std::map& evals, std::vector& terms, Expr eval, const Datatype& dt, size_t i, size_t j ) { const DatatypeConstructor& ctor = dt[j]; Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl; @@ -567,7 +587,11 @@ Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vec Expr builtTerm; //if( ops[i][j].getKind() == kind::BUILTIN ){ if( !builtApply.empty() ){ - builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + if( ops[i][j].getKind() != kind::BUILTIN ){ + builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply); + }else{ + builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + } }else{ builtTerm = ops[i][j]; } @@ -577,7 +601,7 @@ Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vec pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern); assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern); Debug("parser-sygus") << "...made assertion " << assertion << std::endl; - + //linearize multiplication if possible if( builtTerm.getKind()==kind::MULT ){ for(size_t k = 0; k < ctor.getNumArgs(); ++k) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ca1602f36..ed6a5128b 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -183,11 +183,14 @@ public: } void defineSygusFuns(); - + + void mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, + std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs ); + // i is index in datatypes/ops // j is index is datatype - Expr getSygusAssertion( std::vector& datatypeTypes, std::vector< std::vector >& ops, - std::map& evals, std::vector& terms, + Expr getSygusAssertion( std::vector& datatypeTypes, std::vector< std::vector >& ops, + std::map& evals, std::vector& terms, Expr eval, const Datatype& dt, size_t i, size_t j ); void addSygusConstraint(Expr constraint) { diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index e6dce35e0..6aeb8cda0 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -27,6 +27,16 @@ using namespace std; namespace CVC4 { +void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) { + if( n.getKind()==OR ){ + for( unsigned i=0; id_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj->d_candidates ) ); Trace("cegqi") << "Base instantiation is : " << d_conj->d_base_inst << std::endl; if( getTermDatabase()->isQAttrSygus( q ) ){ - if( d_conj->d_base_inst.getKind()==NOT && d_conj->d_base_inst[0].getKind()==FORALL ){ - for( unsigned j=0; jd_base_inst[0][0].getNumChildren(); j++ ){ - d_conj->d_inner_vars.push_back( d_conj->d_base_inst[0][0][j] ); + collectDisjuncts( d_conj->d_base_inst, d_conj->d_base_disj ); + Trace("cegqi") << "Conjecture has " << d_conj->d_base_disj.size() << " disjuncts." << std::endl; + //store the inner variables for each disjunct + for( unsigned j=0; jd_base_disj.size(); j++ ){ + d_conj->d_inner_vars_disj.push_back( std::vector< Node >() ); + //if the disjunct is an existential, store it + if( d_conj->d_base_disj[j].getKind()==NOT && d_conj->d_base_disj[j][0].getKind()==FORALL ){ + for( unsigned k=0; kd_base_disj[j][0][0].getNumChildren(); k++ ){ + d_conj->d_inner_vars.push_back( d_conj->d_base_disj[j][0][0][k] ); + d_conj->d_inner_vars_disj[j].push_back( d_conj->d_base_disj[j][0][0][k] ); + } } } d_conj->d_syntax_guided = true; @@ -229,19 +247,38 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { }else{ //must get a counterexample to the value of the current candidate Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); - inst = Rewriter::rewrite( inst ); - //if body is existential, immediately skolemize - Node inst_sk; - if( inst.getKind()==NOT && inst[0].getKind()==FORALL ){ - inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ).negate(); - }else{ - inst_sk = inst; + //check whether we will run CEGIS on inner skolem variables + bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 ); + if( sk_refine ){ + conj->d_ce_sk.push_back( std::vector< Node >() ); } - Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl; - d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) ); - if( !conj->isGround() || conj->d_refine_count==0 ){ - conj->d_ce_sk.push_back( inst[0] ); + std::vector< Node > ic; + ic.push_back( q.negate() ); + std::vector< Node > d; + collectDisjuncts( inst, d ); + Assert( d.size()==conj->d_base_disj.size() ); + //immediately skolemize inner existentials + for( unsigned i=0; igetSkolemizedBody( dr[0] ).negate() ); + if( sk_refine ){ + conj->d_ce_sk.back().push_back( dr[0] ); + } + }else{ + ic.push_back( dr ); + if( sk_refine ){ + conj->d_ce_sk.back().push_back( Node::null() ); + } + if( !conj->d_inner_vars_disj[i].empty() ){ + Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; + } + } } + Node lem = NodeManager::currentNM()->mkNode( OR, ic ); + lem = Rewriter::rewrite( lem ); + Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem ); Trace("cegqi-engine") << " ...find counterexample." << std::endl; } } @@ -260,19 +297,38 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { }else{ Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; for( unsigned j=0; jd_ce_sk.size(); j++ ){ - Node ce_q = conj->d_ce_sk[j]; - Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[ce_q].size() ); - std::vector< Node > model_values; - if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){ - //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate - Node inst_ce_refine; - if( !conj->d_inner_vars.empty() ){ - inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(), - model_values.begin(), model_values.end() ); + bool success = true; + std::vector< Node > lem_c; + Assert( conj->d_ce_sk[j].size()==conj->d_base_disj.size() ); + for( unsigned k=0; kd_ce_sk[j].size(); k++ ){ + Node ce_q = conj->d_ce_sk[j][k]; + Node c_disj = conj->d_base_disj[k]; + if( !ce_q.isNull() ){ + Assert( !conj->d_inner_vars_disj[k].empty() ); + Assert( conj->d_inner_vars_disj[k].size()==getTermDatabase()->d_skolem_constants[ce_q].size() ); + std::vector< Node > model_values; + if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){ + //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate + Node inst_ce_refine = conj->d_base_disj[k][0][1].substitute( conj->d_inner_vars_disj[k].begin(), conj->d_inner_vars_disj[k].end(), + model_values.begin(), model_values.end() ); + lem_c.push_back( inst_ce_refine ); + }else{ + success = false; + break; + } }else{ - inst_ce_refine = conj->d_base_inst.negate(); + if( conj->d_inner_vars_disj[k].empty() ){ + lem_c.push_back( conj->d_base_disj[k].negate() ); + }else{ + //denegrate case : quantified disjunct was trivially true and does not need to be refined + Trace("cegqi-debug") << "*** skip " << conj->d_base_disj[k] << std::endl; + } } - Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine ); + } + if( success ){ + Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); + lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), lem ); + lem = Rewriter::rewrite( lem ); Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl; Trace("cegqi-engine") << " ...refine candidate." << std::endl; d_quantEngine->addLemma( lem ); diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 4f44c121f..8c74b06f6 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -29,6 +29,9 @@ class CegInstantiation : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; private: + /** collect disjuncts */ + static void collectDisjuncts( Node n, std::vector< Node >& ex ); + /** a synthesis conjecture */ class CegConjecture { public: CegConjecture( context::Context* c ); @@ -42,6 +45,8 @@ private: Node d_guard; /** base instantiation */ Node d_base_inst; + /** expand base inst to disjuncts */ + std::vector< Node > d_base_disj; /** guard split */ Node d_guard_split; /** is syntax-guided */ @@ -49,7 +54,8 @@ private: /** list of constants for quantified formula */ std::vector< Node > d_candidates; /** list of variables on inner quantification */ - std::vector< Node > d_inner_vars; + std::vector< Node > d_inner_vars; + std::vector< std::vector< Node > > d_inner_vars_disj; /** initialize guard */ void initializeGuard( QuantifiersEngine * qe ); /** measure term */ @@ -63,7 +69,7 @@ private: /** is assigned */ bool isAssigned() { return !d_quant.isNull(); } /** current extential quantifeirs whose couterexamples we must refine */ - std::vector< Node > d_ce_sk; + std::vector< std::vector< Node > > d_ce_sk; public: //for fairness /** the cardinality literals */ std::map< int, Node > d_lits;