summaryrefslogtreecommitdiff
path: root/src/parser/smt2
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2')
-rw-r--r--src/parser/smt2/Smt2.g182
-rw-r--r--src/parser/smt2/smt2.cpp67
-rw-r--r--src/parser/smt2/smt2.h29
3 files changed, 50 insertions, 228 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ebf50283d..b8b05f7dd 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -356,8 +356,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
if (PARSER_STATE->sygus())
{
// it is a higher-order universal variable
- PARSER_STATE->mkSygusVar(name, t);
- cmd->reset(new EmptyCommand());
+ Expr func = PARSER_STATE->mkBoundVar(name, t);
+ cmd->reset(new DeclareSygusFunctionCommand(name, func, t));
}
else
{
@@ -605,111 +605,99 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
std::vector<Expr> terms;
std::vector<Expr> sygus_vars;
std::vector<std::pair<std::string, Type> > sortedVarNames;
- SExpr sexpr;
- std::unique_ptr<CVC4::CommandSequence> seq;
Type sygus_ret;
- int startIndex = -1;
Expr synth_fun;
Type sygus_type;
+ bool isInv;
}
: /* declare-var */
DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
sortSymbol[t,CHECK_DECLARED]
- { PARSER_STATE->mkSygusVar(name, t);
- cmd->reset(new EmptyCommand());
+ {
+ Expr var = PARSER_STATE->mkBoundVar(name, t);
+ cmd->reset(new DeclareSygusVarCommand(name, var, t));
}
| /* declare-primed-var */
DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
sortSymbol[t,CHECK_DECLARED]
- { PARSER_STATE->mkSygusVar(name, t, true);
- cmd->reset(new EmptyCommand());
+ {
+ // spurious command, we do not need to create a variable. We only keep
+ // track of the command for sanity checking / dumping
+ cmd->reset(new DeclareSygusPrimedVarCommand(name, t));
}
| /* synth-fun */
- ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } )
+ ( SYNTH_FUN_TOK { isInv = false; }
+ | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); }
+ )
{ PARSER_STATE->checkThatLogicIsSet(); }
symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
- ( sortSymbol[range,CHECK_DECLARED] )? {
- if( range.isNull() ){
+ ( sortSymbol[range,CHECK_DECLARED] )?
+ {
+ if (range.isNull())
+ {
PARSER_STATE->parseError("Must supply return type for synth-fun.");
}
- if( range.isFunction() ){
- PARSER_STATE->parseError("Cannot use synth-fun with function return type.");
+ if (range.isFunction())
+ {
+ PARSER_STATE->parseError(
+ "Cannot use synth-fun with function return type.");
}
- seq.reset(new CommandSequence());
std::vector<Type> var_sorts;
- for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
- sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
- ++i) {
- var_sorts.push_back( (*i).second );
+ for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
+ {
+ var_sorts.push_back(p.second);
}
Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
- Type synth_fun_type;
- if( var_sorts.size()>0 ){
- synth_fun_type = EXPR_MANAGER->mkFunctionType(var_sorts, range);
- }else{
- synth_fun_type = range;
- }
+ Type synth_fun_type = var_sorts.size() > 0
+ ? EXPR_MANAGER->mkFunctionType(var_sorts, range)
+ : range;
// we do not allow overloading for synth fun
synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type);
- // we add a declare function command here
- // this is the single unmuted command in the sequence generated by this smt2 command
- // TODO (as part of #1170) : make this a standard command.
- seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type));
- PARSER_STATE->pushScope(true);
- for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
- sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
- ++i) {
- Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
- sygus_vars.push_back( v );
- }
- Expr bvl;
- if (!sygus_vars.empty())
- {
- bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars);
- }
- // associate this variable list with the synth fun
- std::vector< Expr > attr_val_bvl;
- attr_val_bvl.push_back( bvl );
- Command* cattr_bvl = new SetUserAttributeCommand("sygus-synth-fun-var-list", synth_fun, attr_val_bvl);
- cattr_bvl->setMuted(true);
- PARSER_STATE->preemptCommand(cattr_bvl);
// set the sygus type to be range by default, which is overwritten below
// if a grammar is provided
sygus_type = range;
+ // create new scope for parsing the grammar, if any
+ PARSER_STATE->pushScope(true);
+ for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
+ {
+ sygus_vars.push_back(PARSER_STATE->mkBoundVar(p.first, p.second));
+ }
}
(
// optionally, read the sygus grammar
+ //
+ // the sygus type specifies the required grammar for synth_fun, expressed
+ // as a type
sygusGrammar[sygus_type, sygus_vars, fun]
)?
- { // the sygus sym type specifies the required grammar for synth_fun, expressed as a type
+ {
PARSER_STATE->popScope();
- // store a dummy variable which stands for second-order quantification, linked to synth fun by an attribute
- PARSER_STATE->addSygusFunSymbol(sygus_type, synth_fun);
- cmd->reset(seq.release());
+ Debug("parser-sygus") << "...read synth fun " << fun << std::endl;
+ cmd->reset(
+ new SynthFunCommand(fun, synth_fun, sygus_type, isInv, sygus_vars));
}
| /* constraint */
- CONSTRAINT_TOK {
+ CONSTRAINT_TOK {
PARSER_STATE->checkThatLogicIsSet();
Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
}
term[expr, expr2]
{ Debug("parser-sygus") << "...read constraint " << expr << std::endl;
- PARSER_STATE->addSygusConstraint(expr);
- cmd->reset(new EmptyCommand());
+ cmd->reset(new SygusConstraintCommand(expr));
}
- | INV_CONSTRAINT_TOK {
+ | INV_CONSTRAINT_TOK {
PARSER_STATE->checkThatLogicIsSet();
Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
}
- ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
+ ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
if( !terms.empty() ){
if( !PARSER_STATE->isDefinedFunction(name) ){
std::stringstream ss;
@@ -724,85 +712,14 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 "
"arguments.");
}
- // get variables (regular and their respective primed versions)
- std::vector<Expr> vars, primed_vars;
- PARSER_STATE->getSygusInvVars(terms[0].getType(), vars, primed_vars);
- // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
- for (unsigned i = 0; i < 4; ++i)
- {
- Expr op = terms[i];
- Debug("parser-sygus")
- << "Make inv-constraint term #" << i << " : " << op << " with type "
- << op.getType() << "..." << std::endl;
- std::vector<Expr> children;
- children.push_back(op);
- // transition relation applied over both variable lists
- if (i == 2)
- {
- children.insert(children.end(), vars.begin(), vars.end());
- children.insert(
- children.end(), primed_vars.begin(), primed_vars.end());
- }
- else
- {
- children.insert(children.end(), vars.begin(), vars.end());
- }
- terms[i] = EXPR_MANAGER->mkExpr(i == 0 ? kind::APPLY_UF : kind::APPLY,
- children);
- // make application of Inv on primed variables
- if (i == 0)
- {
- children.clear();
- children.push_back(op);
- children.insert(
- children.end(), primed_vars.begin(), primed_vars.end());
- terms.push_back(EXPR_MANAGER->mkExpr(kind::APPLY_UF, children));
- }
- }
- //make constraints
- std::vector< Expr > conj;
- conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1],
- terms[0] ) );
- const Expr term0_and_2 = EXPR_MANAGER->mkExpr(kind::AND, terms[0],
- terms[2] );
- conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, term0_and_2,
- terms[4] ) );
- conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3]) );
- Expr ic = EXPR_MANAGER->mkExpr( kind::AND, conj );
- Debug("parser-sygus") << "...read invariant constraint " << ic
- << std::endl;
- PARSER_STATE->addSygusConstraint(ic);
- cmd->reset(new EmptyCommand());
+
+ cmd->reset(new SygusInvConstraintCommand(terms));
}
| /* check-synth */
CHECK_SYNTH_TOK
{ PARSER_STATE->checkThatLogicIsSet(); }
- { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
- Expr inst_attr =EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar);
- Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, inst_attr);
- std::vector<Expr> bodyv;
- Debug("parser-sygus") << "Sygus : Constructing sygus constraint..."
- << std::endl;
- Expr body = EXPR_MANAGER->mkExpr(kind::NOT,
- PARSER_STATE->getSygusConstraints());
- Debug("parser-sygus") << "...constructed sygus constraint " << body
- << std::endl;
- if( !PARSER_STATE->getSygusVars().empty() ){
- Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST,
- PARSER_STATE->getSygusVars());
- body = EXPR_MANAGER->mkExpr(kind::EXISTS, boundVars, body);
- Debug("parser-sygus") << "...constructed exists " << body << std::endl;
- }
- if( !PARSER_STATE->getSygusFunSymbols().empty() ){
- Expr boundVars = EXPR_MANAGER->mkExpr(
- kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols());
- body = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, body, sygusAttr);
- }
- Debug("parser-sygus") << "...constructed forall " << body << std::endl;
- Command* c = new SetUserAttributeCommand("sygus", sygusVar);
- c->setMuted(true);
- PARSER_STATE->preemptCommand(c);
- cmd->reset(new CheckSynthCommand(body));
+ {
+ cmd->reset(new CheckSynthCommand());
}
| command[cmd]
;
@@ -818,7 +735,8 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
*/
sygusGrammar[CVC4::Type & ret,
std::vector<CVC4::Expr>& sygus_vars,
- std::string& fun] @declarations
+ std::string& fun]
+@declarations
{
Type t;
std::string name;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c4046b7c2..2fd61aabc 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -630,20 +630,6 @@ void Smt2::includeFile(const std::string& filename) {
}
}
-void Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
-{
- if (!isPrimed)
- {
- d_sygusVars.push_back(mkBoundVar(name, type));
- }
-#ifdef CVC4_ASSERTIONS
- else
- {
- d_sygusVarPrimed.push_back(mkBoundVar(name, type));
- }
-#endif
-}
-
void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
if( type.isInteger() ){
ops.push_back(getExprManager()->mkConst(Rational(0)));
@@ -1234,59 +1220,6 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt,
return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
}
-const void Smt2::getSygusInvVars(FunctionType t,
- std::vector<Expr>& vars,
- std::vector<Expr>& primed_vars)
-{
- std::vector<Type> argTypes = t.getArgTypes();
- ExprManager* em = getExprManager();
- for (const Type& ti : argTypes)
- {
- vars.push_back(em->mkBoundVar(ti));
- d_sygusVars.push_back(vars.back());
- std::stringstream ss;
- ss << vars.back() << "'";
- primed_vars.push_back(em->mkBoundVar(ss.str(), ti));
- d_sygusVars.push_back(primed_vars.back());
-#ifdef CVC4_ASSERTIONS
- bool find_new_declared_var = false;
- for (const Expr& e : d_sygusVarPrimed)
- {
- if (e.getType() == ti)
- {
- d_sygusVarPrimed.erase(
- std::find(d_sygusVarPrimed.begin(), d_sygusVarPrimed.end(), e));
- find_new_declared_var = true;
- break;
- }
- }
- if (!find_new_declared_var)
- {
- ss.str("");
- ss << "warning: decleared primed variables do not match invariant's "
- "type\n";
- warning(ss.str());
- }
-#endif
- }
-}
-
-const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
- // When constructing the synthesis conjecture, we quantify on the
- // (higher-order) bound variable synth_fun.
- d_sygusFunSymbols.push_back(synth_fun);
-
- // Variable "sfproxy" carries the type, which may be a SyGuS datatype
- // that corresponds to syntactic restrictions.
- Expr sym = mkBoundVar("sfproxy", t);
- std::vector< Expr > attr_value;
- attr_value.push_back(sym);
- Command* cattr =
- new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value);
- cattr->setMuted(true);
- preemptCommand(cattr);
-}
-
InputLanguage Smt2::getLanguage() const
{
ExprManager* em = getExprManager();
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 80bd8df83..2d57332af 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -273,35 +273,6 @@ private:
std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin );
- void addSygusConstraint(Expr constraint) {
- d_sygusConstraints.push_back(constraint);
- }
-
- Expr getSygusConstraints() {
- switch(d_sygusConstraints.size()) {
- case 0: return getExprManager()->mkConst(bool(true));
- case 1: return d_sygusConstraints[0];
- default: return getExprManager()->mkExpr(kind::AND, d_sygusConstraints);
- }
- }
-
- const std::vector<Expr>& getSygusVars() {
- return d_sygusVars;
- }
- /** retrieves the invariant variables (both regular and primed)
- *
- * To ensure that the variable list represent the correct argument type order
- * the type of the invariant predicate is used during the variable retrieval
- */
- const void getSygusInvVars(FunctionType t,
- std::vector<Expr>& vars,
- std::vector<Expr>& primed_vars);
-
- const void addSygusFunSymbol( Type t, Expr synth_fun );
- const std::vector<Expr>& getSygusFunSymbols() {
- return d_sygusFunSymbols;
- }
-
/**
* Smt2 parser provides its own checkDeclaration, which does the
* same as the base, but with some more helpful errors.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback