CommandSequence* seq;
std::vector<CVC4::Datatype> datatypes;
std::vector< std::vector<Expr> > 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]
sorts.push_back(t);
datatypes.push_back(Datatype(dname));
ops.push_back(std::vector<Expr>());
+ cnames.push_back(std::vector<std::string>());
+ cargs.push_back(std::vector<std::vector<CVC4::Type> >());
if(!PARSER_STATE->isUnresolvedType(dname)) {
// if not unresolved, must be undeclared
PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
}
// 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();
// 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<CVC4::Expr>& ops]
+sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs]
@declarations {
std::string name;
Kind k;
}
: 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]
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 >() );
}
}
;
//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<Expr> applyv;
}
}
+void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
+ std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) {
+ //minimize grammar goes here
+
+ for( unsigned i=0; i<cnames.size(); i++ ){
+ std::string name = dt.getName() + "_" + cnames[i];
+ std::string testerId("is-");
+ testerId.append(name);
+ checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+ checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+ CVC4::DatatypeConstructor c(name, testerId);
+ for( unsigned j=0; j<cargs[i].size(); j++ ){
+ std::stringstream sname;
+ sname << name << "_" << j;
+ c.addArg(sname.str(), cargs[i][j]);
+ }
+ dt.addConstructor(c);
+ }
+}
+
// i is index in datatypes/ops
// j is index is datatype
-Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
- std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
+Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
+ std::map<DatatypeType, Expr>& evals, std::vector<Expr>& 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;
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];
}
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) {
}
void defineSygusFuns();
-
+
+ void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
+ std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs );
+
// i is index in datatypes/ops
// j is index is datatype
- Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
- std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
+ Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
+ std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
Expr eval, const Datatype& dt, size_t i, size_t j );
void addSygusConstraint(Expr constraint) {
namespace CVC4 {
+void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
+ if( n.getKind()==OR ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ collectDisjuncts( n[i], d );
+ }
+ }else{
+ d.push_back( n );
+ }
+}
+
CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
d_refine_count = 0;
}
d_conj->d_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; j<d_conj->d_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; j<d_conj->d_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; k<d_conj->d_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;
}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; i<d.size(); i++ ){
+ Node dr = Rewriter::rewrite( d[i] );
+ if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
+ ic.push_back( getTermDatabase()->getSkolemizedBody( 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;
}
}
}else{
Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl;
for( unsigned j=0; j<conj->d_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; k<conj->d_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 );
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
+ /** collect disjuncts */
+ static void collectDisjuncts( Node n, std::vector< Node >& ex );
+ /** a synthesis conjecture */
class CegConjecture {
public:
CegConjecture( context::Context* c );
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 */
/** 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 */
/** 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;
projects / cvc5.git / commitdiff