From: ajreynol Date: Fri, 16 Jan 2015 11:38:08 +0000 (+0100) Subject: Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare... X-Git-Tag: cvc5-1.0.0~6440 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb54542531904204fc147015469d54c6750ab73b;p=cvc5.git Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 67f26533e..3f999366d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -636,8 +636,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] 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 bvs, extraArgs; for(size_t k = 0; k < ctor.getNumArgs(); ++k) { std::string vname = "v_" + ctor[k].getName(); @@ -647,6 +649,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } 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 patv; patv.push_back(eval); std::vector applyv; @@ -654,9 +657,12 @@ sygusCommand returns [CVC4::Command* cmd = NULL] 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 builtApply; for(size_t k = 0; k < extraArgs.size(); ++k) { patv.clear(); @@ -667,11 +673,19 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } 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)); } } @@ -679,9 +693,13 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } | /* 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 */ @@ -689,9 +707,15 @@ sygusCommand returns [CVC4::Command* cmd = NULL] { 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 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); @@ -722,13 +746,15 @@ sygusGTerm[CVC4::Datatype& dt, std::vector& ops] ( 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; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 50edc3311..35842f308 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -187,41 +187,55 @@ public: while(d_nextSygusFun < d_sygusFuns.size()) { std::pair 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 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 sygusVars; std::vector 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 sygusVars; - std::vector types; + //std::vector 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 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; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 1b02b2a13..e6dce35e0 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -28,7 +28,7 @@ using namespace std; 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 ) { @@ -113,10 +113,10 @@ void CegInstantiation::registerQuantifier( 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; jd_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; jd_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 ) ){ @@ -230,14 +230,18 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { //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; } } @@ -261,12 +265,18 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { 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(); diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 235f2b01c..4f44c121f 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -56,6 +56,8 @@ private: 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 */ @@ -69,6 +71,8 @@ private: 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; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e04e76835..fc59b22b7 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -196,6 +196,10 @@ option ceGuidedInst --cegqi bool :default false :read-write 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 diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index be58919db..efa12b893 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1158,9 +1158,10 @@ void TermDb::computeAttributes( Node q ) { 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 ){