DatatypeType dtt = datatypeTypes[i];
const Datatype& dt = dtt.getDatatype();
Expr eval = evals[dtt];
+ Debug("parser-sygus") << "Sygus : process grammar : " << dt << std::endl;
for(size_t j = 0; j < dt.getNumConstructors(); ++j) {
const DatatypeConstructor& ctor = dt[j];
+ Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
std::vector<Expr> bvs, extraArgs;
for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
std::string vname = "v_" + ctor[k].getName();
}
bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, bvs);
+ Debug("parser-sygus") << "...made bv list." << std::endl;
std::vector<Expr> patv;
patv.push_back(eval);
std::vector<Expr> applyv;
applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end());
for(size_t k = 0; k < applyv.size(); ++k) {
}
- patv.push_back(MK_EXPR(kind::APPLY_CONSTRUCTOR, applyv));
+ Expr cpatv = MK_EXPR(kind::APPLY_CONSTRUCTOR, applyv);
+ Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl;
+ patv.push_back(cpatv);
patv.insert(patv.end(), terms[0].begin(), terms[0].end());
Expr evalApply = MK_EXPR(kind::APPLY_UF, patv);
+ Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
std::vector<Expr> builtApply;
for(size_t k = 0; k < extraArgs.size(); ++k) {
patv.clear();
}
for(size_t k = 0; k < builtApply.size(); ++k) {
}
- Expr builtTerm = ops[i][j].getKind() == kind::BUILTIN ? MK_EXPR(ops[i][j], builtApply) : ops[i][j];
+ Expr builtTerm;
+ //if( ops[i][j].getKind() == kind::BUILTIN ){
+ if( !builtApply.empty() ){
+ builtTerm = MK_EXPR(ops[i][j], builtApply);
+ }else{
+ builtTerm = ops[i][j];
+ }
+ Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
Expr assertion = MK_EXPR(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
Expr pattern = MK_EXPR(kind::INST_PATTERN, evalApply);
pattern = MK_EXPR(kind::INST_PATTERN_LIST, pattern);
assertion = MK_EXPR(kind::FORALL, bvl, assertion, pattern);
+ Debug("parser-sygus") << "Add assertion " << assertion << std::endl;
seq->addCommand(new AssertCommand(assertion));
}
}
}
| /* constraint */
CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { PARSER_STATE->defineSygusFuns(); }
+ { Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
+ PARSER_STATE->defineSygusFuns();
+ Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
+ }
term[expr, expr2]
- { PARSER_STATE->addSygusConstraint(expr);
+ { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
+ PARSER_STATE->addSygusConstraint(expr);
$cmd = new EmptyCommand();
}
| /* check-synth */
{ Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar));
std::vector<Expr> bodyv;
+ Debug("parser-sygus") << "Sygus : Constructing sygus constraint..." << std::endl;
Expr body = EXPR_MANAGER->mkExpr(kind::NOT, PARSER_STATE->getSygusConstraints());
- body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body);
+ Debug("parser-sygus") << "...constructed sygus constraint " << body << std::endl;
+ if( !PARSER_STATE->getSygusVars().empty() ){
+ body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body);
+ Debug("parser-sygus") << "...constructed exists " << body << std::endl;
+ }
body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+ Debug("parser-sygus") << "...constructed forall " << body << std::endl;
Command* c = new SetUserAttributeCommand("sygus", sygusVar);
c->setMuted(true);
PARSER_STATE->preemptCommand(c);
( builtinOp[k]
{ ops.push_back(EXPR_MANAGER->operatorOf(k));
name = kind::kindToString(k);
+ Debug("parser-sygus") << "Sygus : grammar builtin symbol : " << name << std::endl;
}
- | symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+ | 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 symbol : " << name << std::endl;
}
)
{ name = dt.getName() + "_" + name;
while(d_nextSygusFun < d_sygusFuns.size()) {
std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
std::string fun = p.first;
+ Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl;
Expr eval = p.second;
FunctionType evalType = eval.getType();
std::vector<Type> argTypes = evalType.getArgTypes();
Type rangeType = evalType.getRangeType();
+ Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl;
// first make the function type
+ std::vector<Expr> sygusVars;
std::vector<Type> funType;
for(size_t j = 1; j < argTypes.size(); ++j) {
funType.push_back(argTypes[j]);
+ std::stringstream ss;
+ ss << fun << "_v_" << j;
+ sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j]));
}
Type funt = getExprManager()->mkFunctionType(funType, rangeType);
+ Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
// copy the bound vars
+ /*
std::vector<Expr> sygusVars;
- std::vector<Type> types;
+ //std::vector<Type> types;
for(size_t i = 0; i < d_sygusVars.size(); ++i) {
std::stringstream ss;
ss << d_sygusVars[i];
Type type = d_sygusVars[i].getType();
sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
- types.push_back(type);
+ //types.push_back(type);
}
-
- Type t = getExprManager()->mkFunctionType(types, rangeType);
- Expr lambda = mkFunction(fun, t, ExprManager::VAR_FLAG_DEFINED);
+ Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
+ */
+
+ //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;
Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]);
d_sygusFunSymbols.push_back(funbv);
applyv.push_back(eval);
applyv.push_back(funbv);
- for(size_t i = 0; i < d_sygusVars.size(); ++i) {
- applyv.push_back(d_sygusVars[i]);
+ for(size_t i = 0; i < sygusVars.size(); ++i) {
+ applyv.push_back(sygusVars[i]);
}
Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
- Command* cmd = new DefineFunctionCommand(fun, lambda, d_sygusVars, apply);
+ Debug("parser-sygus") << "...made apply " << apply << std::endl;
+ Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
preemptCommand(cmd);
++d_nextSygusFun;
namespace CVC4 {
CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
-
+ d_refine_count = 0;
}
void CegInstantiation::CegConjecture::assign( Node q ) {
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 ) ){
- Assert( d_conj->d_base_inst.getKind()==NOT );
- Assert( 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] );
+ 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] );
+ }
}
d_conj->d_syntax_guided = true;
}else if( getTermDatabase()->isQAttrSynthesis( q ) ){
//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 );
- //body should be an existential
- Assert( inst.getKind()==NOT );
- Assert( inst[0].getKind()==FORALL );
- //immediately skolemize
- Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ).negate();
+ //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;
+ }
Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) );
- conj->d_ce_sk.push_back( inst[0] );
+ if( !conj->isGround() || conj->d_refine_count==0 ){
+ conj->d_ce_sk.push_back( inst[0] );
+ }
Trace("cegqi-engine") << " ...find counterexample." << std::endl;
}
}
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_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
- model_values.begin(), model_values.end() );
+ 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() );
+ }else{
+ inst_ce_refine = conj->d_base_inst.negate();
+ }
Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine );
Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
Trace("cegqi-engine") << " ...refine candidate." << std::endl;
d_quantEngine->addLemma( lem );
+ conj->d_refine_count++;
}
}
conj->d_ce_sk.clear();
Node d_measure_term;
/** measure sum size */
int d_measure_term_size;
+ /** refine count */
+ unsigned d_refine_count;
/** assign */
void assign( Node q );
/** is assigned */
context::CDO< int > d_curr_lit;
/** allocate literal */
Node getLiteral( QuantifiersEngine * qe, int i );
+ /** is ground */
+ bool isGround() { return d_inner_vars.empty(); }
};
/** the quantified formula stating the synthesis conjecture */
CegConjecture * d_conj;
counterexample-guided quantifier instantiation
option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
if and how to apply fairness for cegqi
+option sygusMinGrammar --sygus-min-grammar bool :default false
+ minimize sygus grammars
+option sygusDecompose --sygus-decompose bool :default false
+ decompose single invocation synthesis conjectures
option localTheoryExt --local-t-ext bool :default false
d_fun_defs[f] = true;
}
if( avar.getAttribute(SygusAttribute()) ){
- //should be nested existential
- Assert( q[1].getKind()==NOT );
- Assert( q[1][0].getKind()==FORALL );
+ //not necessarily nested existential
+ //Assert( q[1].getKind()==NOT );
+ //Assert( q[1][0].getKind()==FORALL );
+
Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
d_qattr_sygus[q] = true;
if( d_quantEngine->getCegInstantiation()==NULL ){
projects / cvc5.git / commitdiff