summaryrefslogtreecommitdiff
path: root/src/parser/smt2
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-03-05 16:16:15 -0600
committerGitHub <noreply@github.com>2020-03-05 16:16:15 -0600
commit500f85f9c664001b84a90f4836bbb9577b871e29 (patch)
treebe92a8a20267fe7d381ba1a6cf6c9477825776bf /src/parser/smt2
parent50f82fac417bc5b27ecaeb34d4e8034339c5982f (diff)
Migrate a majority of the functionality in parsers to the new API (#3838)
This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout. Remaining tasks: Migrate the Datatypes to the new API in cvc/smt2. Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL). For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc. Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version. This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r--src/parser/smt2/Smt2.g588
-rw-r--r--src/parser/smt2/smt2.cpp980
-rw-r--r--src/parser/smt2/smt2.h166
-rw-r--r--src/parser/smt2/smt2_input.cpp2
-rw-r--r--src/parser/smt2/sygus_input.cpp2
5 files changed, 892 insertions, 846 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9ae9f7261..cd661364d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -87,24 +87,26 @@ using namespace CVC4::parser;
namespace CVC4 {
class Expr;
+ namespace api {
+ class Term;
+ class Sort;
+ }
+
namespace parser {
namespace smt2 {
/**
* Just exists to provide the uintptr_t constructor that ANTLR
* requires.
*/
- struct myExpr : public CVC4::Expr {
- myExpr() : CVC4::Expr() {}
- myExpr(void*) : CVC4::Expr() {}
- myExpr(const Expr& e) : CVC4::Expr(e) {}
- myExpr(const myExpr& e) : CVC4::Expr(e) {}
+ struct myExpr : public CVC4::api::Term {
+ myExpr() : CVC4::api::Term() {}
+ myExpr(void*) : CVC4::api::Term() {}
+ myExpr(const Expr& e) : CVC4::api::Term(e) {}
+ myExpr(const myExpr& e) : CVC4::api::Term(e) {}
};/* struct myExpr */
}/* CVC4::parser::smt2 namespace */
}/* CVC4::parser namespace */
- namespace api {
- class Term;
- }
}/* CVC4 namespace */
}/* @parser::includes */
@@ -141,14 +143,10 @@ using namespace CVC4::parser;
* PARSER would be undefined.) */
#undef PARSER_STATE
#define PARSER_STATE ((Smt2*)PARSER->super)
-#undef EXPR_MANAGER
-#define EXPR_MANAGER PARSER_STATE->getExprManager()
-#undef MK_EXPR
-#define MK_EXPR EXPR_MANAGER->mkExpr
-#undef MK_CONST
-#define MK_CONST EXPR_MANAGER->mkConst
#undef SOLVER
#define SOLVER PARSER_STATE->getSolver()
+#undef MK_TERM
+#define MK_TERM SOLVER->mkTerm
#define UNSUPPORTED PARSER_STATE->unimplementedFeature
}/* parser::postinclude */
@@ -160,7 +158,7 @@ using namespace CVC4::parser;
*/
parseExpr returns [CVC4::parser::smt2::myExpr expr]
@declarations {
- Expr expr2;
+ CVC4::api::Term expr2;
}
: term[expr, expr2]
| EOF
@@ -225,12 +223,12 @@ command [std::unique_ptr<CVC4::Command>* cmd]
@declarations {
std::string name;
std::vector<std::string> names;
- Expr expr, expr2;
- Type t;
- std::vector<Expr> terms;
- std::vector<Type> sorts;
- std::vector<std::pair<std::string, Type> > sortedVarNames;
- std::vector<Expr> flattenVars;
+ CVC4::api::Term expr, expr2;
+ CVC4::api::Sort t;
+ std::vector<CVC4::api::Term> terms;
+ std::vector<api::Sort> sorts;
+ std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
+ std::vector<CVC4::api::Term> flattenVars;
}
: /* set the logic */
SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
@@ -267,11 +265,11 @@ command [std::unique_ptr<CVC4::Command>* cmd]
<< "' arity=" << n << std::endl;
unsigned arity = AntlrInput::tokenToUnsigned(n);
if(arity == 0) {
- Type type = PARSER_STATE->mkSort(name);
- cmd->reset(new DeclareTypeCommand(name, 0, type));
+ api::Sort type = PARSER_STATE->mkSort(name);
+ cmd->reset(new DeclareTypeCommand(name, 0, type.getType()));
} else {
- Type type = PARSER_STATE->mkSortConstructor(name, arity);
- cmd->reset(new DeclareTypeCommand(name, arity, type));
+ api::Sort type = PARSER_STATE->mkSortConstructor(name, arity);
+ cmd->reset(new DeclareTypeCommand(name, arity, type.getType()));
}
}
| /* sort definition */
@@ -291,8 +289,9 @@ command [std::unique_ptr<CVC4::Command>* cmd]
{ PARSER_STATE->popScope();
// Do NOT call mkSort, since that creates a new sort!
// This name is not its own distinct sort, it's an alias.
- PARSER_STATE->defineParameterizedType(name, sorts, t);
- cmd->reset(new DefineTypeCommand(name, sorts, t));
+ PARSER_STATE->defineParameterizedType(name, sorts, t.getType());
+ cmd->reset(new DefineTypeCommand(
+ name, api::sortVectorToTypes(sorts), t.getType()));
}
| /* function declaration */
DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -315,8 +314,9 @@ command [std::unique_ptr<CVC4::Command>* cmd]
if (PARSER_STATE->sygus_v1())
{
// it is a higher-order universal variable
- Expr func = PARSER_STATE->mkBoundVar(name, t);
- cmd->reset(new DeclareSygusFunctionCommand(name, func, t));
+ api::Term func = PARSER_STATE->bindBoundVar(name, t);
+ cmd->reset(
+ new DeclareSygusFunctionCommand(name, func.getExpr(), t.getType()));
}
else if( PARSER_STATE->sygus() )
{
@@ -325,8 +325,10 @@ command [std::unique_ptr<CVC4::Command>* cmd]
}
else
{
- Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
- cmd->reset(new DeclareFunctionCommand(name, func, t));
+ api::Term func =
+ PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+ cmd->reset(
+ new DeclareFunctionCommand(name, func.getExpr(), t.getType()));
}
}
| /* function definition */
@@ -339,7 +341,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
Debug("parser") << "define fun: '" << name << "'" << std::endl;
if( sortedVarNames.size() > 0 ) {
sorts.reserve(sortedVarNames.size());
- for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+ for(std::vector<std::pair<std::string, api::Sort> >::const_iterator i =
sortedVarNames.begin(), iend = sortedVarNames.end();
i != iend;
++i) {
@@ -348,7 +350,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
}
PARSER_STATE->pushScope(true);
- terms = PARSER_STATE->mkBoundVars(sortedVarNames);
+ terms = PARSER_STATE->bindBoundVars(sortedVarNames);
}
term[expr, expr2]
{
@@ -363,16 +365,17 @@ command [std::unique_ptr<CVC4::Command>* cmd]
// must not be extended with the name itself; no recursion
// permitted)
// we allow overloading for function definitions
- Expr func = PARSER_STATE->mkVar(name, t,
+ api::Term func = PARSER_STATE->bindVar(name, t,
ExprManager::VAR_FLAG_DEFINED, true);
- cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
+ cmd->reset(new DefineFunctionCommand(
+ name, func.getExpr(), api::termVectorToExprs(terms), expr.getExpr()));
}
| DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
| DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
| /* value query */
GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( LPAREN_TOK termList[terms,expr] RPAREN_TOK
- { cmd->reset(new GetValueCommand(terms)); }
+ { cmd->reset(new GetValueCommand(api::termVectorToExprs(terms))); }
| ~LPAREN_TOK
{ PARSER_STATE->parseError("The get-value command expects a list of "
"terms. Perhaps you forgot a pair of "
@@ -387,11 +390,13 @@ command [std::unique_ptr<CVC4::Command>* cmd]
{ PARSER_STATE->clearLastNamedTerm(); }
term[expr, expr2]
{ bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
- cmd->reset(new AssertCommand(expr, inUnsatCore));
+ cmd->reset(new AssertCommand(expr.getExpr(), inUnsatCore));
if(inUnsatCore) {
// set the expression name, if there was a named term
- std::pair<Expr, std::string> namedTerm = PARSER_STATE->lastNamedTerm();
- Command* csen = new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
+ std::pair<api::Term, std::string> namedTerm =
+ PARSER_STATE->lastNamedTerm();
+ Command* csen = new SetExpressionNameCommand(namedTerm.first.getExpr(),
+ namedTerm.second);
csen->setMuted(true);
PARSER_STATE->preemptCommand(csen);
}
@@ -409,13 +414,15 @@ command [std::unique_ptr<CVC4::Command>* cmd]
"permitted while operating in strict compliance mode.");
}
}
- | { expr = Expr(); }
+ | { expr = api::Term(); }
)
- { cmd->reset(new CheckSatCommand(expr)); }
+ { cmd->reset(new CheckSatCommand(expr.getExpr())); }
| /* check-sat-assuming */
CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( LPAREN_TOK termList[terms,expr] RPAREN_TOK
- { cmd->reset(new CheckSatAssumingCommand(terms)); }
+ {
+ cmd->reset(new CheckSatAssumingCommand(api::termVectorToExprs(terms)));
+ }
| ~LPAREN_TOK
{ PARSER_STATE->parseError("The check-sat-assuming command expects a "
"list of terms. Perhaps you forgot a pair of "
@@ -544,14 +551,14 @@ command [std::unique_ptr<CVC4::Command>* cmd]
sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
@declarations {
- Expr expr, expr2;
- Type t, range;
+ CVC4::api::Term expr, expr2;
+ CVC4::api::Sort t, range;
std::vector<std::string> names;
- std::vector<std::pair<std::string, Type> > sortedVarNames;
+ std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory;
std::string name, fun;
bool isInv;
- Type grammar;
+ CVC4::api::Sort grammar;
}
: /* declare-var */
DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -559,8 +566,8 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
{ PARSER_STATE->checkUserSymbol(name); }
sortSymbol[t,CHECK_DECLARED]
{
- Expr var = PARSER_STATE->mkBoundVar(name, t);
- cmd.reset(new DeclareSygusVarCommand(name, var, t));
+ api::Term var = PARSER_STATE->bindBoundVar(name, t);
+ cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType()));
}
| /* declare-primed-var */
DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -570,12 +577,12 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
{
// 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));
+ cmd.reset(new DeclareSygusPrimedVarCommand(name, t.getType()));
}
| /* synth-fun */
( SYNTH_FUN_V1_TOK { isInv = false; }
- | SYNTH_INV_V1_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); }
+ | SYNTH_INV_V1_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
)
{ PARSER_STATE->checkThatLogicIsSet(); }
symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -597,7 +604,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
}
| /* synth-fun */
( SYNTH_FUN_TOK { isInv = false; }
- | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); }
+ | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
)
{ PARSER_STATE->checkThatLogicIsSet(); }
symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -625,7 +632,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
}
term[expr, expr2]
{ Debug("parser-sygus") << "...read constraint " << expr << std::endl;
- cmd.reset(new SygusConstraintCommand(expr));
+ cmd.reset(new SygusConstraintCommand(expr.getExpr()));
}
| /* inv-constraint */
INV_CONSTRAINT_TOK
@@ -651,24 +658,24 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
* The argument fun is a unique identifier to avoid naming clashes for the
* datatypes constructed by this call.
*/
-sygusGrammarV1[CVC4::Type & ret,
- const std::vector<CVC4::Expr>& sygus_vars,
+sygusGrammarV1[CVC4::api::Sort & ret,
+ const std::vector<CVC4::api::Term>& sygus_vars,
const std::string& fun]
@declarations
{
- Type t;
+ CVC4::api::Sort t;
std::string name;
unsigned startIndex = 0;
std::vector<std::vector<CVC4::SygusGTerm>> sgts;
std::vector<CVC4::Datatype> datatypes;
- std::vector<Type> sorts;
+ std::vector<api::Sort> sorts;
std::vector<std::vector<ParseOp>> ops;
std::vector<std::vector<std::string>> cnames;
- std::vector<std::vector<std::vector<CVC4::Type>>> cargs;
+ std::vector<std::vector<std::vector<CVC4::api::Sort>>> cargs;
std::vector<bool> allow_const;
std::vector<std::vector<std::string>> unresolved_gterm_sym;
- std::map<CVC4::Type, CVC4::Type> sygus_to_builtin;
- std::map<CVC4::Type, CVC4::Expr> sygus_to_builtin_expr;
+ std::map<CVC4::api::Sort, CVC4::api::Sort> sygus_to_builtin;
+ std::map<CVC4::api::Sort, CVC4::api::Term> sygus_to_builtin_expr;
}
: LPAREN_TOK { PARSER_STATE->pushScope(); }
(LPAREN_TOK
@@ -688,7 +695,7 @@ sygusGrammarV1[CVC4::Type & ret,
cargs,
allow_const,
unresolved_gterm_sym);
- Type unres_t;
+ api::Sort unres_t;
if (!PARSER_STATE->isUnresolvedType(name))
{
// if not unresolved, must be undeclared
@@ -724,7 +731,7 @@ sygusGrammarV1[CVC4::Type & ret,
{
for (unsigned j = 0, size = sgts[i].size(); j < size; j++)
{
- Type sub_ret;
+ api::Sort sub_ret;
PARSER_STATE->processSygusGTerm(sgts[i][j],
i,
datatypes,
@@ -748,10 +755,10 @@ sygusGrammarV1[CVC4::Type & ret,
Debug("parser-sygus") << "..." << datatypes[i].getName()
<< " has builtin sort " << sorts[i] << std::endl;
}
- Expr bvl;
+ api::Term bvl;
if (!sygus_vars.empty())
{
- bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars);
+ bvl = MK_TERM(api::BOUND_VAR_LIST, sygus_vars);
}
for (unsigned i = 0; i < ndatatypes; i++)
{
@@ -763,7 +770,8 @@ sygusGrammarV1[CVC4::Type & ret,
"Internal error : could not infer "
"builtin sort for nested gterm.");
}
- datatypes[i].setSygus(sorts[i], bvl, allow_const[i], false);
+ datatypes[i].setSygus(
+ sorts[i].getType(), bvl.getExpr(), allow_const[i], false);
PARSER_STATE->mkSygusDatatype(datatypes[i],
ops[i],
cnames[i],
@@ -796,10 +804,10 @@ sygusGrammarV1[CVC4::Type & ret,
sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
@declarations {
std::string name, name2;
- Kind k;
- Type t;
+ CVC4::api::Kind k;
+ CVC4::api::Sort t;
std::string sname;
- std::vector< Expr > let_vars;
+ std::vector< CVC4::api::Term > let_vars;
std::string s;
CVC4::api::Term atomTerm;
}
@@ -833,7 +841,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : "
<< name << std::endl;
k = PARSER_STATE->getOperatorKind(name);
- sgt.d_name = kind::kindToString(k);
+ sgt.d_name = api::kindToString(k);
sgt.d_gterm_type = SygusGTerm::gterm_op;
sgt.d_op.d_kind = k;
}else{
@@ -886,7 +894,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
Debug("parser-sygus") << "Sygus grammar " << fun
<< " : unary minus integer literal " << name
<< std::endl;
- sgt.d_op.d_expr = MK_CONST(Rational(name));
+ sgt.d_op.d_expr = SOLVER->mkReal(name);
sgt.d_name = name;
sgt.d_gterm_type = SygusGTerm::gterm_op;
}else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
@@ -922,21 +930,21 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
* The argument fun is a unique identifier to avoid naming clashes for the
* datatypes constructed by this call.
*/
-sygusGrammar[CVC4::Type & ret,
- const std::vector<CVC4::Expr>& sygusVars,
+sygusGrammar[CVC4::api::Sort & ret,
+ const std::vector<CVC4::api::Term>& sygusVars,
const std::string& fun]
@declarations
{
// the pre-declaration
- std::vector<std::pair<std::string, Type> > sortedVarNames;
+ std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
// non-terminal symbols of the grammar
- std::vector<Expr> ntSyms;
- Type t;
+ std::vector<CVC4::api::Term> ntSyms;
+ CVC4::api::Sort t;
std::string name;
- Expr e, e2;
+ CVC4::api::Term e, e2;
std::vector<CVC4::Datatype> datatypes;
- std::vector<Type> unresTypes;
- std::map<Expr, CVC4::Type> ntsToUnres;
+ std::vector<api::Sort> unresTypes;
+ std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres;
unsigned dtProcessed = 0;
std::unordered_set<unsigned> allowConst;
}
@@ -946,20 +954,20 @@ sygusGrammar[CVC4::Type & ret,
{
// non-terminal symbols in the pre-declaration are locally scoped
PARSER_STATE->pushScope(true);
- for (std::pair<std::string, CVC4::Type>& i : sortedVarNames)
+ for (std::pair<std::string, api::Sort>& i : sortedVarNames)
{
Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
// make the datatype, which encodes terms generated by this non-terminal
std::string dname = i.first;
- datatypes.push_back(Datatype(EXPR_MANAGER, dname));
+ datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), dname));
// make its unresolved type, used for referencing the final version of
// the datatype
PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
- Type urt = PARSER_STATE->mkUnresolvedType(dname);
+ api::Sort urt = PARSER_STATE->mkUnresolvedType(dname);
unresTypes.push_back(urt);
// make the non-terminal symbol, which will be parsed as an ordinary
// free variable.
- Expr nts = PARSER_STATE->mkBoundVar(i.first, i.second);
+ api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
ntSyms.push_back(nts);
ntsToUnres[nts] = urt;
}
@@ -1019,17 +1027,17 @@ sygusGrammar[CVC4::Type & ret,
"Number of grouped rule listings does not match "
"number of symbols in predeclaration.");
}
- Expr bvl;
+ api::Term bvl;
if (!sygusVars.empty())
{
- bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygusVars);
+ bvl = MK_TERM(api::BOUND_VAR_LIST, sygusVars);
}
Trace("parser-sygus2") << "Process " << dtProcessed << " sygus datatypes..." << std::endl;
for (unsigned i = 0; i < dtProcessed; i++)
{
bool aci = allowConst.find(i)!=allowConst.end();
- Type btt = sortedVarNames[i].second;
- datatypes[i].setSygus(btt, bvl, aci, false);
+ api::Sort btt = sortedVarNames[i].second;
+ datatypes[i].setSygus(btt.getType(), bvl.getExpr(), aci, false);
Trace("parser-sygus2") << "- " << datatypes[i].getName()
<< ", #cons= " << datatypes[i].getNumConstructors()
<< ", aci= " << aci << std::endl;
@@ -1089,21 +1097,22 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
@declarations {
std::string name;
std::string fname;
- Expr expr, expr2;
- std::vector<std::pair<std::string, Type> > sortedVarNames;
+ CVC4::api::Term expr, expr2;
+ std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
SExpr sexpr;
- Type t;
- Expr func;
- std::vector<Expr> bvs;
- std::vector< std::vector<std::pair<std::string, Type> > > sortedVarNamesList;
- std::vector<std::vector<Expr>> flattenVarsList;
- std::vector<std::vector<Expr>> formals;
- std::vector<Expr> funcs;
- std::vector<Expr> func_defs;
- Expr aexpr;
+ CVC4::api::Sort t;
+ CVC4::api::Term func;
+ std::vector<CVC4::api::Term> bvs;
+ std::vector<std::vector<std::pair<std::string, CVC4::api::Sort>>>
+ sortedVarNamesList;
+ std::vector<std::vector<CVC4::api::Term>> flattenVarsList;
+ std::vector<std::vector<CVC4::api::Term>> formals;
+ std::vector<CVC4::api::Term> funcs;
+ std::vector<CVC4::api::Term> func_defs;
+ CVC4::api::Term aexpr;
std::unique_ptr<CVC4::CommandSequence> seq;
- std::vector<Type> sorts;
- std::vector<Expr> flattenVars;
+ std::vector<api::Sort> sorts;
+ std::vector<CVC4::api::Term> flattenVars;
}
/* declare-const */
: DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -1111,8 +1120,9 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
{ PARSER_STATE->checkUserSymbol(name); }
sortSymbol[t,CHECK_DECLARED]
{ // allow overloading here
- Expr c = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
- cmd->reset(new DeclareFunctionCommand(name, c, t)); }
+ api::Term c =
+ PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+ cmd->reset(new DeclareFunctionCommand(name, c.getExpr(), t.getType())); }
/* get model */
| GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -1144,15 +1154,18 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
sortSymbol[t,CHECK_DECLARED]
{
- func = PARSER_STATE->mkDefineFunRec(fname, sortedVarNames, t, flattenVars);
- PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, bvs, true );
+ func =
+ PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars);
+ PARSER_STATE->pushDefineFunRecScope(
+ sortedVarNames, func, flattenVars, bvs, true);
}
term[expr, expr2]
{ PARSER_STATE->popScope();
if( !flattenVars.empty() ){
expr = PARSER_STATE->mkHoApply( expr, flattenVars );
}
- cmd->reset(new DefineFunctionRecCommand(func,bvs,expr));
+ cmd->reset(new DefineFunctionRecCommand(
+ func.getExpr(), api::termVectorToExprs(bvs), expr.getExpr()));
}
| DEFINE_FUNS_REC_TOK
{ PARSER_STATE->checkThatLogicIsSet();}
@@ -1164,7 +1177,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
sortSymbol[t,CHECK_DECLARED]
{
flattenVars.clear();
- func = PARSER_STATE->mkDefineFunRec( fname, sortedVarNames, t, flattenVars );
+ func = PARSER_STATE->bindDefineFunRec(
+ fname, sortedVarNames, t, flattenVars);
funcs.push_back( func );
// add to lists (need to remember for when parsing the bodies)
@@ -1214,20 +1228,28 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
"Number of functions defined does not match number listed in "
"define-funs-rec"));
}
- cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs));
+ std::vector<std::vector<Expr>> eformals;
+ for (unsigned i=0, fsize = formals.size(); i<fsize; i++)
+ {
+ eformals.push_back(api::termVectorToExprs(formals[i]));
+ }
+ cmd->reset(
+ new DefineFunctionRecCommand(api::termVectorToExprs(funcs),
+ eformals,
+ api::termVectorToExprs(func_defs)));
}
;
extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
@declarations {
std::vector<CVC4::Datatype> dts;
- Expr e, e2;
- Type t;
+ CVC4::api::Term e, e2;
+ CVC4::api::Sort t;
std::string name;
std::vector<std::string> names;
- std::vector<Expr> terms;
- std::vector<Type> sorts;
- std::vector<std::pair<std::string, Type> > sortedVarNames;
+ std::vector<CVC4::api::Term> terms;
+ std::vector<api::Sort> sorts;
+ std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
std::unique_ptr<CVC4::CommandSequence> seq;
}
/* Extended SMT-LIB set of commands syntax, not permitted in
@@ -1236,6 +1258,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
| DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd]
| DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
| DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
+
/* Support some of Z3's extended SMT-LIB commands */
| DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -1250,8 +1273,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
LPAREN_TOK
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
{ PARSER_STATE->checkUserSymbol(name);
- Type type = PARSER_STATE->mkSort(name);
- seq->addCommand(new DeclareTypeCommand(name, 0, type));
+ api::Sort type = PARSER_STATE->mkSort(name);
+ seq->addCommand(new DeclareTypeCommand(name, 0, type.getType()));
}
)+
RPAREN_TOK
@@ -1263,7 +1286,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
nonemptySortList[sorts] RPAREN_TOK
- { Type tt;
+ { api::Sort tt;
if(sorts.size() > 1) {
if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
PARSER_STATE->parseError(
@@ -1273,15 +1296,17 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
+ " unless option --uf-ho is used");
}
// must flatten
- Type range = sorts.back();
+ api::Sort range = sorts.back();
sorts.pop_back();
tt = PARSER_STATE->mkFlatFunctionType(sorts, range);
} else {
tt = sorts[0];
}
// allow overloading
- Expr func = PARSER_STATE->mkVar(name, tt, ExprManager::VAR_FLAG_NONE, true);
- seq->addCommand(new DeclareFunctionCommand(name, func, tt));
+ api::Term func =
+ PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true);
+ seq->addCommand(
+ new DeclareFunctionCommand(name, func.getExpr(), tt.getType()));
sorts.clear();
}
)+
@@ -1293,7 +1318,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
sortList[sorts] RPAREN_TOK
- { Type boolType = EXPR_MANAGER->booleanType();
+ { t = SOLVER->getBooleanSort();
if(sorts.size() > 0) {
if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
PARSER_STATE->parseError(
@@ -1302,11 +1327,13 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
+ PARSER_STATE->getLogic().getLogicString()
+ " unless option --uf-ho is used");
}
- boolType = EXPR_MANAGER->mkFunctionType(sorts, boolType);
+ t = SOLVER->mkFunctionSort(sorts, t);
}
// allow overloading
- Expr func = PARSER_STATE->mkVar(name, boolType, ExprManager::VAR_FLAG_NONE, true);
- seq->addCommand(new DeclareFunctionCommand(name, func, boolType));
+ api::Term func =
+ PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+ seq->addCommand(
+ new DeclareFunctionCommand(name, func.getExpr(), t.getType()));
sorts.clear();
}
)+
@@ -1317,9 +1344,9 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
term[e,e2]
- { Expr func = PARSER_STATE->mkVar(name, e.getType(),
+ { api::Term func = PARSER_STATE->bindVar(name, e.getSort(),
ExprManager::VAR_FLAG_DEFINED);
- cmd->reset(new DefineFunctionCommand(name, func, e));
+ cmd->reset(new DefineFunctionCommand(name, func.getExpr(), e.getExpr()));
}
| LPAREN_TOK
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -1328,27 +1355,27 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
{ /* add variables to parser state before parsing term */
Debug("parser") << "define fun: '" << name << "'" << std::endl;
PARSER_STATE->pushScope(true);
- terms = PARSER_STATE->mkBoundVars(sortedVarNames);
+ terms = PARSER_STATE->bindBoundVars(sortedVarNames);
}
term[e,e2]
{ PARSER_STATE->popScope();
// declare the name down here (while parsing term, signature
// must not be extended with the name itself; no recursion
// permitted)
- Type tt = e.getType();
+ api::Sort tt = e.getSort();
if( sortedVarNames.size() > 0 ) {
- std::vector<CVC4::Type> types;
- types.reserve(sortedVarNames.size());
- for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
+ sorts.reserve(sortedVarNames.size());
+ for(std::vector<std::pair<std::string, api::Sort> >::const_iterator
i = sortedVarNames.begin(), iend = sortedVarNames.end();
i != iend; ++i) {
- types.push_back((*i).second);
+ sorts.push_back((*i).second);
}
- tt = EXPR_MANAGER->mkFunctionType(types, tt);
+ tt = SOLVER->mkFunctionSort(sorts, tt);
}
- Expr func = PARSER_STATE->mkVar(name, tt,
+ api::Term func = PARSER_STATE->bindVar(name, tt,
ExprManager::VAR_FLAG_DEFINED);
- cmd->reset(new DefineFunctionCommand(name, func, terms, e));
+ cmd->reset(new DefineFunctionCommand(
+ name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr()));
}
)
| DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -1358,37 +1385,38 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
{ /* add variables to parser state before parsing term */
Debug("parser") << "define const: '" << name << "'" << std::endl;
PARSER_STATE->pushScope(true);
- terms = PARSER_STATE->mkBoundVars(sortedVarNames);
+ terms = PARSER_STATE->bindBoundVars(sortedVarNames);
}
term[e, e2]
{ PARSER_STATE->popScope();
// declare the name down here (while parsing term, signature
// must not be extended with the name itself; no recursion
// permitted)
- Expr func = PARSER_STATE->mkVar(name, t,
+ api::Term func = PARSER_STATE->bindVar(name, t,
ExprManager::VAR_FLAG_DEFINED);
- cmd->reset(new DefineFunctionCommand(name, func, terms, e));
+ cmd->reset(new DefineFunctionCommand(
+ name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr()));
}
| SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[e,e2]
- { cmd->reset(new SimplifyCommand(e)); }
+ { cmd->reset(new SimplifyCommand(e.getExpr())); }
| GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[e,e2]
- { cmd->reset(new GetQuantifierEliminationCommand(e, true)); }
+ { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), true)); }
| GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[e,e2]
- { cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
- | GET_ABDUCT_TOK {
+ { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), false)); }
+ | GET_ABDUCT_TOK {
PARSER_STATE->checkThatLogicIsSet();
}
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
term[e,e2]
(
sygusGrammar[t, terms, name]
- )?
+ )?
{
- cmd->reset(new GetAbductCommand(name,e, t));
+ cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType()));
}
| DECLARE_HEAP LPAREN_TOK
sortSymbol[t, CHECK_DECLARED]
@@ -1401,7 +1429,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
| BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( LPAREN_TOK termList[terms,e] RPAREN_TOK
- { cmd->reset(new BlockModelValuesCommand(terms)); }
+ { cmd->reset(new BlockModelValuesCommand(api::termVectorToExprs(terms))); }
| ~LPAREN_TOK
{ PARSER_STATE->parseError("The block-model-value command expects a list "
"of terms. Perhaps you forgot a pair of "
@@ -1415,7 +1443,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
@declarations {
std::vector<CVC4::Datatype> dts;
std::string name;
- std::vector<Type> sorts;
+ std::vector<api::Sort> sorts;
std::vector<std::string> dnames;
std::vector<unsigned> arities;
}
@@ -1424,7 +1452,9 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
PARSER_STATE->pushScope(true); }
LPAREN_TOK /* parametric sorts */
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
- { sorts.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); }
+ {
+ sorts.push_back(PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER));
+ }
)*
RPAREN_TOK
LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
@@ -1483,7 +1513,7 @@ datatypesDef[bool isCo,
@declarations {
std::vector<CVC4::Datatype> dts;
std::string name;
- std::vector<Type> params;
+ std::vector<api::Sort> params;
}
: { PARSER_STATE->pushScope(true); }
( LPAREN_TOK {
@@ -1495,7 +1525,8 @@ datatypesDef[bool isCo,
}
( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
- { params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); }
+ {
+ params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); }
)*
RPAREN_TOK {
// if the arity was fixed by prelude and is not equal to the number of parameters
@@ -1503,7 +1534,7 @@ datatypesDef[bool isCo,
PARSER_STATE->parseError("Wrong number of parameters for datatype.");
}
Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
- dts.push_back(Datatype(EXPR_MANAGER, dnames[dts.size()],params,isCo));
+ dts.push_back(Datatype(PARSER_STATE->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo));
}
LPAREN_TOK
( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
@@ -1513,7 +1544,10 @@ datatypesDef[bool isCo,
PARSER_STATE->parseError("No parameters given for datatype.");
}
Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
- dts.push_back(Datatype(EXPR_MANAGER, dnames[dts.size()],params,isCo));
+ dts.push_back(Datatype(PARSER_STATE->getExprManager(),
+ dnames[dts.size()],
+ api::sortVectorToTypes(params),
+ isCo));
}
( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
)
@@ -1586,12 +1620,12 @@ symbolicExpr[CVC4::SExpr& sexpr]
* Matches a term.
* @return the expression representing the term.
*/
-term[CVC4::Expr& expr, CVC4::Expr& expr2]
+term[CVC4::api::Term& expr, CVC4::api::Term& expr2]
@init {
- Kind kind = kind::NULL_EXPR;
- Expr f;
+ api::Kind kind = api::NULL_EXPR;
+ CVC4::api::Term f;
std::string name;
- Type type;
+ CVC4::api::Sort type;
ParseOp p;
}
: termNonVariable[expr, expr2]
@@ -1609,26 +1643,26 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
* @return the expression expr representing the term or formula, and expr2, an
* optional annotation for expr (for instance, for attributed expressions).
*/
-termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
+termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
@init {
Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
- Kind kind = kind::NULL_EXPR;
+ api::Kind kind = api::NULL_EXPR;
std::string name;
- std::vector<Expr> args;
- std::vector< std::pair<std::string, Type> > sortedVarNames;
- Expr bvl;
- Expr f, f2, f3;
+ std::vector<CVC4::api::Term> args;
+ std::vector< std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
+ CVC4::api::Term bvl;
+ CVC4::api::Term f, f2, f3;
std::string attr;
- Expr attexpr;
- std::vector<Expr> patexprs;
- std::vector<Expr> matchcases;
+ CVC4::api::Term attexpr;
+ std::vector<CVC4::api::Term> patexprs;
+ std::vector<CVC4::api::Term> matchcases;
std::unordered_set<std::string> names;
- std::vector< std::pair<std::string, Expr> > binders;
- Type type;
- Type type2;
+ std::vector< std::pair<std::string, CVC4::api::Term> > binders;
+ CVC4::api::Sort type;
+ CVC4::api::Sort type2;
api::Term atomTerm;
ParseOp p;
- std::vector<Type> argTypes;
+ std::vector<api::Sort> argTypes;
}
: LPAREN_TOK quantOp[kind]
{ PARSER_STATE->pushScope(true); }
@@ -1642,7 +1676,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
if(! f2.isNull()){
args.push_back(f2);
}
- expr = MK_EXPR(kind, args);
+ expr = MK_TERM(kind, args);
}
| LPAREN_TOK COMPREHENSION_TOK
{ PARSER_STATE->pushScope(true); }
@@ -1651,9 +1685,9 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
args.push_back(bvl);
}
term[f, f2] { args.push_back(f); }
- term[f, f2] {
- args.push_back(f);
- expr = MK_EXPR(CVC4::kind::COMPREHENSION, args);
+ term[f, f2] {
+ args.push_back(f);
+ expr = MK_TERM(api::COMPREHENSION, args);
}
RPAREN_TOK
| LPAREN_TOK qualIdentifier[p]
@@ -1697,7 +1731,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
}
binders.push_back(std::make_pair(name, expr)); } )+ )
{ // now implement these bindings
- for (const std::pair<std::string, Expr>& binder : binders)
+ for (const std::pair<std::string, api::Term>& binder : binders)
{
{
PARSER_STATE->defineVar(binder.first, binder.second);
@@ -1710,7 +1744,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
{ PARSER_STATE->popScope(); }
| /* match expression */
LPAREN_TOK MATCH_TOK term[expr, f2] {
- if( !expr.getType().isDatatype() ){
+ if( !expr.getSort().isDatatype() ){
PARSER_STATE->parseError("Cannot match on non-datatype term.");
}
}
@@ -1721,17 +1755,19 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
args.clear();
PARSER_STATE->pushScope(true);
// f should be a constructor
- type = f.getType();
+ type = f.getSort();
Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
if (!type.isConstructor())
{
PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
}
- if (Datatype::datatypeOf(f).isParametric())
+ Expr ef = f.getExpr();
+ if (Datatype::datatypeOf(ef).isParametric())
{
- type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType());
+ type = Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
+ .getSpecializedConstructorType(expr.getSort().getType());
}
- argTypes = static_cast<ConstructorType>(type).getArgTypes();
+ argTypes = type.getConstructorDomainSorts();
}
// arguments of the pattern
( symbol[name,CHECK_NONE,SYM_VARIABLE] {
@@ -1740,18 +1776,18 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
PARSER_STATE->parseError("Too many arguments for pattern.");
}
//make of proper type
- Expr arg = PARSER_STATE->mkBoundVar(name, argTypes[args.size()]);
+ api::Term arg = PARSER_STATE->bindBoundVar(name, argTypes[args.size()]);
args.push_back( arg );
}
)*
RPAREN_TOK term[f3, f2] {
// make the match case
- std::vector<Expr> cargs;
+ std::vector<CVC4::api::Term> cargs;
cargs.push_back(f);
cargs.insert(cargs.end(),args.begin(),args.end());
- Expr c = MK_EXPR(kind::APPLY_CONSTRUCTOR,cargs);
- Expr bvla = MK_EXPR(kind::BOUND_VAR_LIST,args);
- Expr mc = MK_EXPR(kind::MATCH_BIND_CASE, bvla, c, f3);
+ api::Term c = MK_TERM(api::APPLY_CONSTRUCTOR,cargs);
+ api::Term bvla = MK_TERM(api::BOUND_VAR_LIST,args);
+ api::Term mc = MK_TERM(api::MATCH_BIND_CASE, bvla, c, f3);
matchcases.push_back(mc);
// now, pop the scope
PARSER_STATE->popScope();
@@ -1762,31 +1798,31 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
if (PARSER_STATE->isDeclared(name,SYM_VARIABLE))
{
f = PARSER_STATE->getVariable(name);
- type = f.getType();
- if (!type.isConstructor() ||
- !((ConstructorType)type).getArgTypes().empty())
+ type = f.getSort();
+ if (!type.isConstructor() ||
+ !type.getConstructorDomainSorts().empty())
{
PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
}
// make nullary constructor application
- f = MK_EXPR(kind::APPLY_CONSTRUCTOR, f);
+ f = MK_TERM(api::APPLY_CONSTRUCTOR, f);
}
else
{
// it has the type of the head expr
- f = PARSER_STATE->mkBoundVar(name, expr.getType());
+ f = PARSER_STATE->bindBoundVar(name, expr.getSort());
}
}
term[f3, f2] {
- Expr mc;
- if (f.getKind() == kind::BOUND_VARIABLE)
+ api::Term mc;
+ if (f.getKind() == api::VARIABLE)
{
- Expr bvlf = MK_EXPR(kind::BOUND_VAR_LIST, f);
- mc = MK_EXPR(kind::MATCH_BIND_CASE, bvlf, f, f3);
+ api::Term bvlf = MK_TERM(api::BOUND_VAR_LIST, f);
+ mc = MK_TERM(api::MATCH_BIND_CASE, bvlf, f, f3);
}
else
{
- mc = MK_EXPR(kind::MATCH_CASE, f, f3);
+ mc = MK_TERM(api::MATCH_CASE, f, f3);
}
matchcases.push_back(mc);
}
@@ -1798,10 +1834,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
{
PARSER_STATE->parseError("Must have at least one case in match.");
}
- std::vector<Expr> mchildren;
+ std::vector<api::Term> mchildren;
mchildren.push_back(expr);
mchildren.insert(mchildren.end(), matchcases.begin(), matchcases.end());
- expr = MK_EXPR(kind::MATCH, mchildren);
+ expr = MK_TERM(api::MATCH, mchildren);
}
/* attributed expressions */
@@ -1814,9 +1850,9 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
)+ RPAREN_TOK
{
if(! patexprs.empty()) {
- if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){
+ if( !f2.isNull() && f2.getKind()==api::INST_PATTERN_LIST ){
for( size_t i=0; i<f2.getNumChildren(); i++ ){
- if( f2[i].getKind()==kind::INST_PATTERN ){
+ if( f2[i].getKind()==api::INST_PATTERN ){
patexprs.push_back( f2[i] );
}else{
std::stringstream ss;
@@ -1826,7 +1862,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
}
}
}
- expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs);
+ expr2 = MK_TERM(api::INST_PATTERN_LIST, patexprs);
} else {
expr2 = f2;
}
@@ -1840,15 +1876,15 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
args.push_back(bvl);
args.push_back(f);
PARSER_STATE->popScope();
- expr = MK_EXPR(CVC4::kind::LAMBDA, args);
+ expr = MK_TERM(api::LAMBDA, args);
}
| LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
{
std::vector<api::Sort> sorts;
std::vector<api::Term> terms;
- for (const Expr& arg : args)
+ for (const api::Term& arg : args)
{
- sorts.emplace_back(arg.getType());
+ sorts.emplace_back(arg.getSort());
terms.emplace_back(arg);
}
expr = SOLVER->mkTuple(sorts, terms).getExpr();
@@ -1881,7 +1917,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
* - For declared functions f, we return (2).
* - For indexed functions like testers (_ is C) and bitvector extract
* (_ extract n m), we return (3) for the appropriate operator.
- * - For tuple selectors (_ tupSel n), we return (1) and (3). Kind is set to
+ * - For tuple selectors (_ tupSel n), we return (1) and (3). api::Kind is set to
* APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
* caller as the n^th generic tuple selector. We do this since there is no
* AST expression representing generic tuple select, and we do not have enough
@@ -1910,16 +1946,16 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
*/
qualIdentifier[CVC4::ParseOp& p]
@init {
- Kind k;
+ api::Kind k;
std::string baseName;
- Expr f;
- Type type;
+ CVC4::api::Term f;
+ CVC4::api::Sort type;
}
: identifier[p]
| LPAREN_TOK AS_TOK
( CONST_TOK sortSymbol[type, CHECK_DECLARED]
{
- p.d_kind = kind::STORE_ALL;
+ p.d_kind = api::STORE_ALL;
PARSER_STATE->parseOpApplyTypeAscription(p, type);
}
| identifier[p]
@@ -1941,8 +1977,8 @@ qualIdentifier[CVC4::ParseOp& p]
*/
identifier[CVC4::ParseOp& p]
@init {
- Expr f;
- Expr f2;
+ CVC4::api::Term f;
+ CVC4::api::Term f2;
std::vector<uint64_t> numerals;
}
: functionName[p.d_name, CHECK_NONE]
@@ -1952,24 +1988,29 @@ identifier[CVC4::ParseOp& p]
| LPAREN_TOK INDEX_TOK
( TESTER_TOK term[f, f2]
{
- if (f.getKind() == kind::APPLY_CONSTRUCTOR && f.getNumChildren() == 0)
+ if (f.getKind() == api::APPLY_CONSTRUCTOR && f.getNumChildren() == 1)
{
// for nullary constructors, must get the operator
- f = f.getOperator();
+ f = f[0];
}
- if (!f.getType().isConstructor())
+ if (!f.getSort().isConstructor())
{
PARSER_STATE->parseError(
"Bad syntax for test (_ is X), X must be a constructor.");
}
- p.d_expr = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getTester();
+ // get the datatype that f belongs to
+ api::Sort sf = f.getSort().getConstructorCodomainSort();
+ api::Datatype d = sf.getDatatype();
+ // lookup by name
+ api::DatatypeConstructor dc = d.getConstructor(f.toString());
+ p.d_expr = dc.getTesterTerm();
}
| TUPLE_SEL_TOK m=INTEGER_LITERAL
{
// we adopt a special syntax (_ tupSel n)
- p.d_kind = CVC4::kind::APPLY_SELECTOR;
+ p.d_kind = api::APPLY_SELECTOR;
// put m in expr so that the caller can deal with this case
- p.d_expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
+ p.d_expr = SOLVER->mkReal(AntlrInput::tokenToUnsigned($m));
}
| sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
{
@@ -1985,8 +2026,8 @@ identifier[CVC4::ParseOp& p]
*/
termAtomic[CVC4::api::Term& atomTerm]
@init {
- Type type;
- Type type2;
+ CVC4::api::Sort type;
+ CVC4::api::Sort type2;
std::string s;
std::vector<uint64_t> numerals;
}
@@ -2054,18 +2095,17 @@ termAtomic[CVC4::api::Term& atomTerm]
/**
* Read attribute
*/
-attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
+attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
@init {
SExpr sexpr;
- Expr patexpr;
- std::vector<Expr> patexprs;
- Expr e2;
+ CVC4::api::Term patexpr;
+ std::vector<CVC4::api::Term> patexprs;
+ CVC4::api::Term e2;
bool hasValue = false;
}
: KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
{
attr = AntlrInput::tokenText($KEYWORD);
- // EXPR_MANAGER->setNamedAttribute( expr, attr );
if(attr == ":rewrite-rule") {
if(hasValue) {
std::stringstream ss;
@@ -2083,18 +2123,18 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
<< " does not take a value (ignoring)";
PARSER_STATE->warning(ss.str());
}
- Expr avar;
+ api::Term avar;
bool success = true;
std::string attr_name = attr;
attr_name.erase( attr_name.begin() );
if( attr==":fun-def" ){
- if( expr.getKind()!=kind::EQUAL || expr[0].getKind()!=kind::APPLY_UF ){
+ if( expr.getKind()!=api::EQUAL || expr[0].getKind()!=api::APPLY_UF ){
success = false;
}else{
- FunctionType t = (FunctionType)expr[0].getOperator().getType();
+ api::Sort t = expr[0].getOp().getSort();
for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){
- if( expr[0][i].getKind() != kind::BOUND_VARIABLE ||
- expr[0][i].getType() != t.getArgTypes()[i] ){
+ if( expr[0][i].getKind() != api::VARIABLE ||
+ expr[0][i].getSort() != t.getFunctionDomainSorts()[i] ){
success = false;
break;
}else{
@@ -2116,14 +2156,14 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
avar = expr[0];
}
}else{
- Type boolType = EXPR_MANAGER->booleanType();
- avar = PARSER_STATE->mkVar(attr_name, boolType);
+ api::Sort boolType = SOLVER->getBooleanSort();
+ avar = PARSER_STATE->bindVar(attr_name, boolType);
}
if( success ){
//Will set the attribute on auxiliary var (preserves attribute on
//formula through rewriting).
- retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
- Command* c = new SetUserAttributeCommand( attr_name, avar );
+ retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
+ Command* c = new SetUserAttributeCommand( attr_name, avar.getExpr() );
c->setMuted(true);
PARSER_STATE->preemptCommand(c);
}
@@ -2137,35 +2177,38 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
)+ RPAREN_TOK
{
attr = std::string(":pattern");
- retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
+ retExpr = MK_TERM(api::INST_PATTERN, patexprs);
}
| ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2]
{
attr = std::string(":no-pattern");
- retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr);
+ retExpr = MK_TERM(api::INST_NO_PATTERN, patexpr);
}
- | tok=( ATTRIBUTE_INST_LEVEL | ATTRIBUTE_RR_PRIORITY ) INTEGER_LITERAL
+ | tok=( ATTRIBUTE_INST_LEVEL ) INTEGER_LITERAL
{
- Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) );
- std::vector<Expr> values;
+ std::stringstream sIntLit;
+ sIntLit << $INTEGER_LITERAL;
+ api::Term n = SOLVER->mkReal(sIntLit.str());
+ std::vector<api::Term> values;
values.push_back( n );
std::string attr_name(AntlrInput::tokenText($tok));
attr_name.erase( attr_name.begin() );
- Type boolType = EXPR_MANAGER->booleanType();
- Expr avar = PARSER_STATE->mkVar(attr_name, boolType);
- retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
- Command* c = new SetUserAttributeCommand( attr_name, avar, values );
+ api::Sort boolType = SOLVER->getBooleanSort();
+ api::Term avar = PARSER_STATE->bindVar(attr_name, boolType);
+ retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
+ Command* c = new SetUserAttributeCommand(
+ attr_name, avar.getExpr(), api::termVectorToExprs(values));
c->setMuted(true);
PARSER_STATE->preemptCommand(c);
}
| ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
{
attr = std::string(":named");
- Expr func = PARSER_STATE->setNamedAttribute(expr, sexpr);
+ api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr);
std::string name = sexpr.getValue();
// bind name to expr with define-fun
- Command* c =
- new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
+ Command* c = new DefineNamedFunctionCommand(
+ name, func.getExpr(), std::vector<Expr>(), expr.getExpr());
c->setMuted(true);
PARSER_STATE->preemptCommand(c);
}
@@ -2175,13 +2218,13 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
* Matches a sequence of terms and puts them into the formulas
* vector.
* @param formulas the vector to fill with terms
- * @param expr an Expr reference for the elements of the sequence
+ * @param expr an CVC4::api::Term reference for the elements of the sequence
*/
-/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
+/* NOTE: We pass an CVC4::api::Term in here just to avoid allocating a fresh CVC4::api::Term every
* time through this rule. */
-termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
+termList[std::vector<CVC4::api::Term>& formulas, CVC4::api::Term& expr]
@declarations {
- Expr expr2;
+ CVC4::api::Term expr2;
}
: ( term[expr, expr2] { formulas.push_back(expr); } )+
;
@@ -2236,12 +2279,12 @@ str[std::string& s, bool fsmtlib]
}
;
-quantOp[CVC4::Kind& kind]
+quantOp[CVC4::api::Kind& kind]
@init {
Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : EXISTS_TOK { $kind = CVC4::kind::EXISTS; }
- | FORALL_TOK { $kind = CVC4::kind::FORALL; }
+ : EXISTS_TOK { $kind = api::EXISTS; }
+ | FORALL_TOK { $kind = api::FORALL; }
;
/**
@@ -2256,16 +2299,16 @@ functionName[std::string& name, CVC4::parser::DeclarationCheck check]
* Matches a sequence of sort symbols and fills them into the given
* vector.
*/
-sortList[std::vector<CVC4::Type>& sorts]
+sortList[std::vector<CVC4::api::Sort>& sorts]
@declarations {
- Type t;
+ CVC4::api::Sort t;
}
: ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
;
-nonemptySortList[std::vector<CVC4::Type>& sorts]
+nonemptySortList[std::vector<CVC4::api::Sort>& sorts]
@declarations {
- Type t;
+ CVC4::api::Sort t;
}
: ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
;
@@ -2274,10 +2317,10 @@ nonemptySortList[std::vector<CVC4::Type>& sorts]
* Matches a sequence of (variable,sort) symbol pairs and fills them
* into the given vector.
*/
-sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
+sortedVarList[std::vector<std::pair<std::string, CVC4::api::Sort> >& sortedVars]
@declarations {
std::string name;
- Type t;
+ CVC4::api::Sort t;
}
: ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
@@ -2289,14 +2332,15 @@ sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
* Matches a sequence of (variable, sort) symbol pairs, registers them as bound
* variables, and returns a term corresponding to the list of pairs.
*/
-boundVarList[CVC4::Expr& expr]
+boundVarList[CVC4::api::Term& expr]
@declarations {
- std::vector<std::pair<std::string, CVC4::Type>> sortedVarNames;
+ std::vector<std::pair<std::string, CVC4::api::Sort>> sortedVarNames;
}
: LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
{
- std::vector<CVC4::Expr> args = PARSER_STATE->mkBoundVars(sortedVarNames);
- expr = MK_EXPR(kind::BOUND_VAR_LIST, args);
+ std::vector<CVC4::api::Term> args =
+ PARSER_STATE->bindBoundVars(sortedVarNames);
+ expr = MK_TERM(api::BOUND_VAR_LIST, args);
}
;
@@ -2308,10 +2352,10 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check]
: symbol[name,check,SYM_SORT]
;
-sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
+sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check]
@declarations {
std::string name;
- std::vector<CVC4::Type> args;
+ std::vector<CVC4::api::Sort> args;
std::vector<uint64_t> numerals;
bool indexed = false;
}
@@ -2340,7 +2384,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
if(numerals.front() == 0) {
PARSER_STATE->parseError("Illegal bitvector size: 0");
}
- t = EXPR_MANAGER->mkBitVectorType(numerals.front());
+ t = SOLVER->mkBitVectorSort(numerals.front());
} else if ( name == "FloatingPoint" ) {
if( numerals.size() != 2 ) {
PARSER_STATE->parseError("Illegal floating-point type.");
@@ -2351,7 +2395,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
if(!validSignificandSize(numerals[1])) {
PARSER_STATE->parseError("Illegal floating-point significand size");
}
- t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]);
+ t = SOLVER->mkFloatingPointSort(numerals[0],numerals[1]);
} else {
std::stringstream ss;
ss << "unknown indexed sort symbol `" << name << "'";
@@ -2373,15 +2417,15 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
if(args.size() != 2) {
PARSER_STATE->parseError("Illegal array type.");
}
- t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
+ t = SOLVER->mkArraySort( args[0], args[1] );
} else if(name == "Set" &&
PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
if(args.size() != 1) {
PARSER_STATE->parseError("Illegal set type.");
}
- t = EXPR_MANAGER->mkSetType( args[0] );
+ t = SOLVER->mkSetSort( args[0] );
} else if(name == "Tuple") {
- t = EXPR_MANAGER->mkTupleType(args);
+ t = SOLVER->mkTupleSort(args);
} else if(check == CHECK_DECLARED ||
PARSER_STATE->isDeclared(name, SYM_SORT)) {
t = PARSER_STATE->getSort(name, args);
@@ -2393,7 +2437,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
<< std::endl;
} else {
t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
- t = SortConstructorType(t).instantiate( args );
+ t = t.instantiate( args );
Debug("parser-param")
<< "param: make unres param type " << name << " " << args.size()
<< " " << PARSER_STATE->getArity( name ) << std::endl;
@@ -2407,7 +2451,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
PARSER_STATE->parseError("Arrow types must have at least 2 arguments");
}
//flatten the type
- Type rangeType = args.back();
+ api::Sort rangeType = args.back();
args.pop_back();
t = PARSER_STATE->mkFlatFunctionType( args, rangeType );
}
@@ -2474,7 +2518,7 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals]
* Parses a datatype definition
*/
datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
- std::vector< CVC4::Type >& params]
+ std::vector< CVC4::api::Sort >& params]
@init {
std::string id;
}
@@ -2483,11 +2527,11 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
* "defined" as an unresolved type; don't worry, we check
* below. */
: symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
- { datatypes.push_back(Datatype(EXPR_MANAGER, id, params, isCo));
- if(!PARSER_STATE->isUnresolvedType(id)) {
- // if not unresolved, must be undeclared
- PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
- }
+ {
+ datatypes.push_back(Datatype(PARSER_STATE->getExprManager(),
+ id,
+ api::sortVectorToTypes(params),
+ isCo));
}
( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
{ PARSER_STATE->popScope(); }
@@ -2518,10 +2562,10 @@ constructorDef[CVC4::Datatype& type]
selector[CVC4::DatatypeConstructor& ctor]
@init {
std::string id;
- Type t, t2;
+ CVC4::api::Sort t, t2;
}
: symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
- { ctor.addArg(id, t);
+ { ctor.addArg(id, t.getType());
Debug("parser-idt") << "selector: " << id.c_str()
<< " of type " << t << std::endl;
}
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 15fdd8461..73be8910f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -45,242 +45,236 @@ Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
}
void Smt2::addArithmeticOperators() {
- addOperator(kind::PLUS, "+");
- addOperator(kind::MINUS, "-");
- // kind::MINUS is converted to kind::UMINUS if there is only a single operand
- Parser::addOperator(kind::UMINUS);
- addOperator(kind::MULT, "*");
- addOperator(kind::LT, "<");
- addOperator(kind::LEQ, "<=");
- addOperator(kind::GT, ">");
- addOperator(kind::GEQ, ">=");
+ addOperator(api::PLUS, "+");
+ addOperator(api::MINUS, "-");
+ // api::MINUS is converted to api::UMINUS if there is only a single operand
+ Parser::addOperator(api::UMINUS);
+ addOperator(api::MULT, "*");
+ addOperator(api::LT, "<");
+ addOperator(api::LEQ, "<=");
+ addOperator(api::GT, ">");
+ addOperator(api::GEQ, ">=");
if (!strictModeEnabled())
{
// NOTE: this operator is non-standard
- addOperator(kind::POW, "^");
+ addOperator(api::POW, "^");
}
}
void Smt2::addTranscendentalOperators()
{
- addOperator(kind::EXPONENTIAL, "exp");
- addOperator(kind::SINE, "sin");
- addOperator(kind::COSINE, "cos");
- addOperator(kind::TANGENT, "tan");
- addOperator(kind::COSECANT, "csc");
- addOperator(kind::SECANT, "sec");
- addOperator(kind::COTANGENT, "cot");
- addOperator(kind::ARCSINE, "arcsin");
- addOperator(kind::ARCCOSINE, "arccos");
- addOperator(kind::ARCTANGENT, "arctan");
- addOperator(kind::ARCCOSECANT, "arccsc");
- addOperator(kind::ARCSECANT, "arcsec");
- addOperator(kind::ARCCOTANGENT, "arccot");
- addOperator(kind::SQRT, "sqrt");
+ addOperator(api::EXPONENTIAL, "exp");
+ addOperator(api::SINE, "sin");
+ addOperator(api::COSINE, "cos");
+ addOperator(api::TANGENT, "tan");
+ addOperator(api::COSECANT, "csc");
+ addOperator(api::SECANT, "sec");
+ addOperator(api::COTANGENT, "cot");
+ addOperator(api::ARCSINE, "arcsin");
+ addOperator(api::ARCCOSINE, "arccos");
+ addOperator(api::ARCTANGENT, "arctan");
+ addOperator(api::ARCCOSECANT, "arccsc");
+ addOperator(api::ARCSECANT, "arcsec");
+ addOperator(api::ARCCOTANGENT, "arccot");
+ addOperator(api::SQRT, "sqrt");
}
void Smt2::addQuantifiersOperators()
{
if (!strictModeEnabled())
{
- addOperator(kind::INST_CLOSURE, "inst-closure");
+ addOperator(api::INST_CLOSURE, "inst-closure");
}
}
void Smt2::addBitvectorOperators() {
- addOperator(kind::BITVECTOR_CONCAT, "concat");
- addOperator(kind::BITVECTOR_NOT, "bvnot");
- addOperator(kind::BITVECTOR_AND, "bvand");
- addOperator(kind::BITVECTOR_OR, "bvor");
- addOperator(kind::BITVECTOR_NEG, "bvneg");
- addOperator(kind::BITVECTOR_PLUS, "bvadd");
- addOperator(kind::BITVECTOR_MULT, "bvmul");
- addOperator(kind::BITVECTOR_UDIV, "bvudiv");
- addOperator(kind::BITVECTOR_UREM, "bvurem");
- addOperator(kind::BITVECTOR_SHL, "bvshl");
- addOperator(kind::BITVECTOR_LSHR, "bvlshr");
- addOperator(kind::BITVECTOR_ULT, "bvult");
- addOperator(kind::BITVECTOR_NAND, "bvnand");
- addOperator(kind::BITVECTOR_NOR, "bvnor");
- addOperator(kind::BITVECTOR_XOR, "bvxor");
- addOperator(kind::BITVECTOR_XNOR, "bvxnor");
- addOperator(kind::BITVECTOR_COMP, "bvcomp");
- addOperator(kind::BITVECTOR_SUB, "bvsub");
- addOperator(kind::BITVECTOR_SDIV, "bvsdiv");
- addOperator(kind::BITVECTOR_SREM, "bvsrem");
- addOperator(kind::BITVECTOR_SMOD, "bvsmod");
- addOperator(kind::BITVECTOR_ASHR, "bvashr");
- addOperator(kind::BITVECTOR_ULE, "bvule");
- addOperator(kind::BITVECTOR_UGT, "bvugt");
- addOperator(kind::BITVECTOR_UGE, "bvuge");
- addOperator(kind::BITVECTOR_SLT, "bvslt");
- addOperator(kind::BITVECTOR_SLE, "bvsle");
- addOperator(kind::BITVECTOR_SGT, "bvsgt");
- addOperator(kind::BITVECTOR_SGE, "bvsge");
- addOperator(kind::BITVECTOR_REDOR, "bvredor");
- addOperator(kind::BITVECTOR_REDAND, "bvredand");
- addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
-
+ addOperator(api::BITVECTOR_CONCAT, "concat");
+ addOperator(api::BITVECTOR_NOT, "bvnot");
+ addOperator(api::BITVECTOR_AND, "bvand");
+ addOperator(api::BITVECTOR_OR, "bvor");
+ addOperator(api::BITVECTOR_NEG, "bvneg");
+ addOperator(api::BITVECTOR_PLUS, "bvadd");
+ addOperator(api::BITVECTOR_MULT, "bvmul");
+ addOperator(api::BITVECTOR_UDIV, "bvudiv");
+ addOperator(api::BITVECTOR_UREM, "bvurem");
+ addOperator(api::BITVECTOR_SHL, "bvshl");
+ addOperator(api::BITVECTOR_LSHR, "bvlshr");
+ addOperator(api::BITVECTOR_ULT, "bvult");
+ addOperator(api::BITVECTOR_NAND, "bvnand");
+ addOperator(api::BITVECTOR_NOR, "bvnor");
+ addOperator(api::BITVECTOR_XOR, "bvxor");
+ addOperator(api::BITVECTOR_XNOR, "bvxnor");
+ addOperator(api::BITVECTOR_COMP, "bvcomp");
+ addOperator(api::BITVECTOR_SUB, "bvsub");
+ addOperator(api::BITVECTOR_SDIV, "bvsdiv");
+ addOperator(api::BITVECTOR_SREM, "bvsrem");
+ addOperator(api::BITVECTOR_SMOD, "bvsmod");
+ addOperator(api::BITVECTOR_ASHR, "bvashr");
+ addOperator(api::BITVECTOR_ULE, "bvule");
+ addOperator(api::BITVECTOR_UGT, "bvugt");
+ addOperator(api::BITVECTOR_UGE, "bvuge");
+ addOperator(api::BITVECTOR_SLT, "bvslt");
+ addOperator(api::BITVECTOR_SLE, "bvsle");
+ addOperator(api::BITVECTOR_SGT, "bvsgt");
+ addOperator(api::BITVECTOR_SGE, "bvsge");
+ addOperator(api::BITVECTOR_REDOR, "bvredor");
+ addOperator(api::BITVECTOR_REDAND, "bvredand");
+ addOperator(api::BITVECTOR_TO_NAT, "bv2nat");
+
+ addIndexedOperator(api::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
+ addIndexedOperator(api::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
addIndexedOperator(
- kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
- addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
+ api::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
addIndexedOperator(
- kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
+ api::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
addIndexedOperator(
- kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
+ api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
addIndexedOperator(
- kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
- addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
- api::BITVECTOR_ROTATE_RIGHT,
- "rotate_right");
- addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
+ api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "rotate_right");
+ addIndexedOperator(api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
}
void Smt2::addDatatypesOperators()
{
- Parser::addOperator(kind::APPLY_CONSTRUCTOR);
- Parser::addOperator(kind::APPLY_TESTER);
- Parser::addOperator(kind::APPLY_SELECTOR);
- Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
+ Parser::addOperator(api::APPLY_CONSTRUCTOR);
+ Parser::addOperator(api::APPLY_TESTER);
+ Parser::addOperator(api::APPLY_SELECTOR);
if (!strictModeEnabled())
{
- addOperator(kind::DT_SIZE, "dt.size");
+ addOperator(api::DT_SIZE, "dt.size");
}
}
void Smt2::addStringOperators() {
- defineVar("re.all",
- getSolver()
- ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())
- .getExpr());
-
- addOperator(kind::STRING_CONCAT, "str.++");
- addOperator(kind::STRING_LENGTH, "str.len");
- addOperator(kind::STRING_SUBSTR, "str.substr" );
- addOperator(kind::STRING_STRCTN, "str.contains" );
- addOperator(kind::STRING_CHARAT, "str.at" );
- addOperator(kind::STRING_STRIDOF, "str.indexof" );
- addOperator(kind::STRING_STRREPL, "str.replace" );
+ defineVar(
+ "re.all",
+ getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma()));
+ addOperator(api::STRING_CONCAT, "str.++");
+ addOperator(api::STRING_LENGTH, "str.len");
+ addOperator(api::STRING_SUBSTR, "str.substr");
+ addOperator(api::STRING_STRCTN, "str.contains");
+ addOperator(api::STRING_CHARAT, "str.at");
+ addOperator(api::STRING_STRIDOF, "str.indexof");
+ addOperator(api::STRING_STRREPL, "str.replace");
if (!strictModeEnabled())
{
- addOperator(kind::STRING_TOLOWER, "str.tolower");
- addOperator(kind::STRING_TOUPPER, "str.toupper");
- addOperator(kind::STRING_REV, "str.rev");
- }
- addOperator(kind::STRING_PREFIX, "str.prefixof" );
- addOperator(kind::STRING_SUFFIX, "str.suffixof" );
- addOperator(kind::STRING_FROM_CODE, "str.from_code");
- addOperator(kind::STRING_IS_DIGIT, "str.is_digit" );
-
+ addOperator(api::STRING_TOLOWER, "str.tolower");
+ addOperator(api::STRING_TOUPPER, "str.toupper");
+ addOperator(api::STRING_REV, "str.rev");
+ }
+ addOperator(api::STRING_PREFIX, "str.prefixof");
+ addOperator(api::STRING_SUFFIX, "str.suffixof");
+ addOperator(api::STRING_FROM_CODE, "str.from_code");
+ addOperator(api::STRING_IS_DIGIT, "str.is_digit");
// at the moment, we only use this syntax for smt2.6.1
if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1
|| getLanguage() == language::input::LANG_SYGUS_V2)
{
- addOperator(kind::STRING_ITOS, "str.from_int");
- addOperator(kind::STRING_STOI, "str.to_int");
- addOperator(kind::STRING_IN_REGEXP, "str.in_re");
- addOperator(kind::STRING_TO_REGEXP, "str.to_re");
- addOperator(kind::STRING_TO_CODE, "str.to_code");
- addOperator(kind::STRING_STRREPLALL, "str.replace_all");
+ addOperator(api::STRING_ITOS, "str.from_int");
+ addOperator(api::STRING_STOI, "str.to_int");
+ addOperator(api::STRING_IN_REGEXP, "str.in_re");
+ addOperator(api::STRING_TO_REGEXP, "str.to_re");
+ addOperator(api::STRING_TO_CODE, "str.to_code");
+ addOperator(api::STRING_STRREPLALL, "str.replace_all");
}
else
{
- addOperator(kind::STRING_ITOS, "int.to.str");
- addOperator(kind::STRING_STOI, "str.to.int");
- addOperator(kind::STRING_IN_REGEXP, "str.in.re");
- addOperator(kind::STRING_TO_REGEXP, "str.to.re");
- addOperator(kind::STRING_TO_CODE, "str.code");
- addOperator(kind::STRING_STRREPLALL, "str.replaceall");
- }
-
- addOperator(kind::REGEXP_CONCAT, "re.++");
- addOperator(kind::REGEXP_UNION, "re.union");
- addOperator(kind::REGEXP_INTER, "re.inter");
- addOperator(kind::REGEXP_STAR, "re.*");
- addOperator(kind::REGEXP_PLUS, "re.+");
- addOperator(kind::REGEXP_OPT, "re.opt");
- addOperator(kind::REGEXP_RANGE, "re.range");
- addOperator(kind::REGEXP_LOOP, "re.loop");
- addOperator(kind::REGEXP_COMPLEMENT, "re.comp");
- addOperator(kind::REGEXP_DIFF, "re.diff");
- addOperator(kind::STRING_LT, "str.<");
- addOperator(kind::STRING_LEQ, "str.<=");
+ addOperator(api::STRING_ITOS, "int.to.str");
+ addOperator(api::STRING_STOI, "str.to.int");
+ addOperator(api::STRING_IN_REGEXP, "str.in.re");
+ addOperator(api::STRING_TO_REGEXP, "str.to.re");
+ addOperator(api::STRING_TO_CODE, "str.code");
+ addOperator(api::STRING_STRREPLALL, "str.replaceall");
+ }
+
+ addOperator(api::REGEXP_CONCAT, "re.++");
+ addOperator(api::REGEXP_UNION, "re.union");
+ addOperator(api::REGEXP_INTER, "re.inter");
+ addOperator(api::REGEXP_STAR, "re.*");
+ addOperator(api::REGEXP_PLUS, "re.+");
+ addOperator(api::REGEXP_OPT, "re.opt");
+ addOperator(api::REGEXP_RANGE, "re.range");
+ addOperator(api::REGEXP_LOOP, "re.loop");
+ addOperator(api::REGEXP_COMPLEMENT, "re.comp");
+ addOperator(api::REGEXP_DIFF, "re.diff");
+ addOperator(api::STRING_LT, "str.<");
+ addOperator(api::STRING_LEQ, "str.<=");
}
void Smt2::addFloatingPointOperators() {
- addOperator(kind::FLOATINGPOINT_FP, "fp");
- addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
- addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
- addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
- addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
- addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
- addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
- addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
- addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
- addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
- addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
- addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
- addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
- addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
- addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
- addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
- addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
- addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
- addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
- addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
- addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
- addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
- addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
- addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
- addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
- addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
-
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
+ addOperator(api::FLOATINGPOINT_FP, "fp");
+ addOperator(api::FLOATINGPOINT_EQ, "fp.eq");
+ addOperator(api::FLOATINGPOINT_ABS, "fp.abs");
+ addOperator(api::FLOATINGPOINT_NEG, "fp.neg");
+ addOperator(api::FLOATINGPOINT_PLUS, "fp.add");
+ addOperator(api::FLOATINGPOINT_SUB, "fp.sub");
+ addOperator(api::FLOATINGPOINT_MULT, "fp.mul");
+ addOperator(api::FLOATINGPOINT_DIV, "fp.div");
+ addOperator(api::FLOATINGPOINT_FMA, "fp.fma");
+ addOperator(api::FLOATINGPOINT_SQRT, "fp.sqrt");
+ addOperator(api::FLOATINGPOINT_REM, "fp.rem");
+ addOperator(api::FLOATINGPOINT_RTI, "fp.roundToIntegral");
+ addOperator(api::FLOATINGPOINT_MIN, "fp.min");
+ addOperator(api::FLOATINGPOINT_MAX, "fp.max");
+ addOperator(api::FLOATINGPOINT_LEQ, "fp.leq");
+ addOperator(api::FLOATINGPOINT_LT, "fp.lt");
+ addOperator(api::FLOATINGPOINT_GEQ, "fp.geq");
+ addOperator(api::FLOATINGPOINT_GT, "fp.gt");
+ addOperator(api::FLOATINGPOINT_ISN, "fp.isNormal");
+ addOperator(api::FLOATINGPOINT_ISSN, "fp.isSubnormal");
+ addOperator(api::FLOATINGPOINT_ISZ, "fp.isZero");
+ addOperator(api::FLOATINGPOINT_ISINF, "fp.isInfinite");
+ addOperator(api::FLOATINGPOINT_ISNAN, "fp.isNaN");
+ addOperator(api::FLOATINGPOINT_ISNEG, "fp.isNegative");
+ addOperator(api::FLOATINGPOINT_ISPOS, "fp.isPositive");
+ addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real");
+
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC,
api::FLOATINGPOINT_TO_FP_GENERIC,
"to_fp");
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
"to_fp_unsigned");
addIndexedOperator(
- kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
+ api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
addIndexedOperator(
- kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
+ api::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
if (!strictModeEnabled())
{
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
"to_fp_bv");
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
"to_fp_fp");
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL,
api::FLOATINGPOINT_TO_FP_REAL,
"to_fp_real");
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
"to_fp_signed");
}
}
void Smt2::addSepOperators() {
- addOperator(kind::SEP_STAR, "sep");
- addOperator(kind::SEP_PTO, "pto");
- addOperator(kind::SEP_WAND, "wand");
- addOperator(kind::SEP_EMP, "emp");
- Parser::addOperator(kind::SEP_STAR);
- Parser::addOperator(kind::SEP_PTO);
- Parser::addOperator(kind::SEP_WAND);
- Parser::addOperator(kind::SEP_EMP);
+ addOperator(api::SEP_STAR, "sep");
+ addOperator(api::SEP_PTO, "pto");
+ addOperator(api::SEP_WAND, "wand");
+ addOperator(api::SEP_EMP, "emp");
+ Parser::addOperator(api::SEP_STAR);
+ Parser::addOperator(api::SEP_PTO);
+ Parser::addOperator(api::SEP_WAND);
+ Parser::addOperator(api::SEP_EMP);
}
void Smt2::addTheory(Theory theory) {
switch(theory) {
case THEORY_ARRAYS:
- addOperator(kind::SELECT, "select");
- addOperator(kind::STORE, "store");
+ addOperator(api::SELECT, "select");
+ addOperator(api::STORE, "store");
break;
case THEORY_BITVECTORS:
@@ -288,145 +282,132 @@ void Smt2::addTheory(Theory theory) {
break;
case THEORY_CORE:
- defineType("Bool", getExprManager()->booleanType());
- defineVar("true", getExprManager()->mkConst(true));
- defineVar("false", getExprManager()->mkConst(false));
- addOperator(kind::AND, "and");
- addOperator(kind::DISTINCT, "distinct");
- addOperator(kind::EQUAL, "=");
- addOperator(kind::IMPLIES, "=>");
- addOperator(kind::ITE, "ite");
- addOperator(kind::NOT, "not");
- addOperator(kind::OR, "or");
- addOperator(kind::XOR, "xor");
+ defineType("Bool", d_solver->getBooleanSort());
+ defineVar("true", d_solver->mkTrue());
+ defineVar("false", d_solver->mkFalse());
+ addOperator(api::AND, "and");
+ addOperator(api::DISTINCT, "distinct");
+ addOperator(api::EQUAL, "=");
+ addOperator(api::IMPLIES, "=>");
+ addOperator(api::ITE, "ite");
+ addOperator(api::NOT, "not");
+ addOperator(api::OR, "or");
+ addOperator(api::XOR, "xor");
break;
case THEORY_REALS_INTS:
- defineType("Real", getExprManager()->realType());
- addOperator(kind::DIVISION, "/");
- addOperator(kind::TO_INTEGER, "to_int");
- addOperator(kind::IS_INTEGER, "is_int");
- addOperator(kind::TO_REAL, "to_real");
+ defineType("Real", d_solver->getRealSort());
+ addOperator(api::DIVISION, "/");
+ addOperator(api::TO_INTEGER, "to_int");
+ addOperator(api::IS_INTEGER, "is_int");
+ addOperator(api::TO_REAL, "to_real");
// falling through on purpose, to add Ints part of Reals_Ints
CVC4_FALLTHROUGH;
case THEORY_INTS:
- defineType("Int", getExprManager()->integerType());
+ defineType("Int", d_solver->getIntegerSort());
addArithmeticOperators();
- addOperator(kind::INTS_DIVISION, "div");
- addOperator(kind::INTS_MODULUS, "mod");
- addOperator(kind::ABS, "abs");
- addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible");
+ addOperator(api::INTS_DIVISION, "div");
+ addOperator(api::INTS_MODULUS, "mod");
+ addOperator(api::ABS, "abs");
+ addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible");
break;
case THEORY_REALS:
- defineType("Real", getExprManager()->realType());
+ defineType("Real", d_solver->getRealSort());
addArithmeticOperators();
- addOperator(kind::DIVISION, "/");
+ addOperator(api::DIVISION, "/");
if (!strictModeEnabled())
{
- addOperator(kind::ABS, "abs");
+ addOperator(api::ABS, "abs");
}
break;
case THEORY_TRANSCENDENTALS:
- defineVar("real.pi",
- getExprManager()->mkNullaryOperator(getExprManager()->realType(),
- CVC4::kind::PI));
+ defineVar("real.pi", d_solver->mkTerm(api::PI));
addTranscendentalOperators();
break;
case THEORY_QUANTIFIERS: addQuantifiersOperators(); break;
case THEORY_SETS:
- defineVar("emptyset",
- d_solver->mkEmptySet(d_solver->getNullSort()).getExpr());
+ defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort()));
// the Boolean sort is a placeholder here since we don't have type info
// without type annotation
- defineVar("univset",
- d_solver->mkUniverseSet(d_solver->getBooleanSort()).getExpr());
-
- addOperator(kind::UNION, "union");
- addOperator(kind::INTERSECTION, "intersection");
- addOperator(kind::SETMINUS, "setminus");
- addOperator(kind::SUBSET, "subset");
- addOperator(kind::MEMBER, "member");
- addOperator(kind::SINGLETON, "singleton");
- addOperator(kind::INSERT, "insert");
- addOperator(kind::CARD, "card");
- addOperator(kind::COMPLEMENT, "complement");
- addOperator(kind::JOIN, "join");
- addOperator(kind::PRODUCT, "product");
- addOperator(kind::TRANSPOSE, "transpose");
- addOperator(kind::TCLOSURE, "tclosure");
+ defineVar("univset", d_solver->mkUniverseSet(d_solver->getBooleanSort()));
+
+ addOperator(api::UNION, "union");
+ addOperator(api::INTERSECTION, "intersection");
+ addOperator(api::SETMINUS, "setminus");
+ addOperator(api::SUBSET, "subset");
+ addOperator(api::MEMBER, "member");
+ addOperator(api::SINGLETON, "singleton");
+ addOperator(api::INSERT, "insert");
+ addOperator(api::CARD, "card");
+ addOperator(api::COMPLEMENT, "complement");
+ addOperator(api::JOIN, "join");
+ addOperator(api::PRODUCT, "product");
+ addOperator(api::TRANSPOSE, "transpose");
+ addOperator(api::TCLOSURE, "tclosure");
break;
case THEORY_DATATYPES:
{
- const std::vector<Type> types;
- defineType("Tuple", getExprManager()->mkTupleType(types));
+ const std::vector<api::Sort> types;
+ defineType("Tuple", d_solver->mkTupleSort(types));
addDatatypesOperators();
break;
}
case THEORY_STRINGS:
- defineType("String", getExprManager()->stringType());
- defineType("RegLan", getExprManager()->regExpType());
- defineType("Int", getExprManager()->integerType());
+ defineType("String", d_solver->getStringSort());
+ defineType("RegLan", d_solver->getRegExpSort());
+ defineType("Int", d_solver->getIntegerSort());
if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
{
- defineVar("re.none", d_solver->mkRegexpEmpty().getExpr());
+ defineVar("re.none", d_solver->mkRegexpEmpty());
}
else
{
- defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
+ defineVar("re.nostr", d_solver->mkRegexpEmpty());
}
- defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr());
+ defineVar("re.allchar", d_solver->mkRegexpSigma());
addStringOperators();
break;
case THEORY_UF:
- Parser::addOperator(kind::APPLY_UF);
+ Parser::addOperator(api::APPLY_UF);
if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
{
- addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card");
- addOperator(kind::CARDINALITY_VALUE, "fmf.card.val");
+ addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card");
+ addOperator(api::CARDINALITY_VALUE, "fmf.card.val");
}
break;
case THEORY_FP:
- defineType("RoundingMode", getExprManager()->roundingModeType());
- defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
- defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
- defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
- defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
-
- defineVar(
- "RNE",
- d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
- defineVar(
- "roundNearestTiesToEven",
- d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
- defineVar(
- "RNA",
- d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
- defineVar(
- "roundNearestTiesToAway",
- d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
- defineVar("RTP",
- d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
+ defineType("RoundingMode", d_solver->getRoundingmodeSort());
+ defineType("Float16", d_solver->mkFloatingPointSort(5, 11));
+ defineType("Float32", d_solver->mkFloatingPointSort(8, 24));
+ defineType("Float64", d_solver->mkFloatingPointSort(11, 53));
+ defineType("Float128", d_solver->mkFloatingPointSort(15, 113));
+
+ defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
+ defineVar("roundNearestTiesToEven",
+ d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
+ defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
+ defineVar("roundNearestTiesToAway",
+ d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
+ defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
defineVar("roundTowardPositive",
- d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
- defineVar("RTN",
- d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
+ defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
defineVar("roundTowardNegative",
- d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
- defineVar("RTZ",
- d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
+ defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
defineVar("roundTowardZero",
- d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
addFloatingPointOperators();
break;
@@ -434,8 +415,7 @@ void Smt2::addTheory(Theory theory) {
case THEORY_SEP:
// the Boolean sort is a placeholder here since we don't have type info
// without type annotation
- defineVar("sep.nil",
- d_solver->mkSepNil(d_solver->getBooleanSort()).getExpr());
+ defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
addSepOperators();
break;
@@ -447,14 +427,15 @@ void Smt2::addTheory(Theory theory) {
}
}
-void Smt2::addOperator(Kind kind, const std::string& name) {
+void Smt2::addOperator(api::Kind kind, const std::string& name)
+{
Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
<< std::endl;
Parser::addOperator(kind);
operatorKindMap[name] = kind;
}
-void Smt2::addIndexedOperator(Kind tKind,
+void Smt2::addIndexedOperator(api::Kind tKind,
api::Kind opKind,
const std::string& name)
{
@@ -462,7 +443,8 @@ void Smt2::addIndexedOperator(Kind tKind,
d_indexedOpKindMap[name] = opKind;
}
-Kind Smt2::getOperatorKind(const std::string& name) const {
+api::Kind Smt2::getOperatorKind(const std::string& name) const
+{
// precondition: isOperatorEnabled(name)
return operatorKindMap.find(name)->second;
}
@@ -513,7 +495,9 @@ bool Smt2::logicIsSet() {
return d_logicSet;
}
-Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
+api::Term Smt2::getExpressionForNameAndType(const std::string& name,
+ api::Sort t)
+{
if (isAbstractValue(name))
{
return mkAbstractValue(name);
@@ -581,40 +565,40 @@ api::Op Smt2::mkIndexedOp(const std::string& name,
return api::Op();
}
-Expr Smt2::mkDefineFunRec(
+api::Term Smt2::bindDefineFunRec(
const std::string& fname,
- const std::vector<std::pair<std::string, Type> >& sortedVarNames,
- Type t,
- std::vector<Expr>& flattenVars)
+ const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
+ api::Sort t,
+ std::vector<api::Term>& flattenVars)
{
- std::vector<Type> sorts;
- for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
+ std::vector<api::Sort> sorts;
+ for (const std::pair<std::string, api::Sort>& svn : sortedVarNames)
{
sorts.push_back(svn.second);
}
// make the flattened function type, add bound variables
// to flattenVars if the defined function was given a function return type.
- Type ft = mkFlatFunctionType(sorts, t, flattenVars);
+ api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars);
// allow overloading
- return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
+ return bindVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
}
void Smt2::pushDefineFunRecScope(
- const std::vector<std::pair<std::string, Type> >& sortedVarNames,
- Expr func,
- const std::vector<Expr>& flattenVars,
- std::vector<Expr>& bvs,
+ const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
+ api::Term func,
+ const std::vector<api::Term>& flattenVars,
+ std::vector<api::Term>& bvs,
bool bindingLevel)
{
pushScope(bindingLevel);
// bound variables are those that are explicitly named in the preamble
// of the define-fun(s)-rec command, we define them here
- for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
+ for (const std::pair<std::string, api::Sort>& svn : sortedVarNames)
{
- Expr v = mkBoundVar(svn.first, svn.second);
+ api::Term v = bindBoundVar(svn.first, svn.second);
bvs.push_back(v);
}
@@ -626,7 +610,7 @@ void Smt2::reset() {
d_seenSetLogic = false;
d_logic = LogicInfo();
operatorKindMap.clear();
- d_lastNamedTerm = std::pair<Expr, std::string>();
+ d_lastNamedTerm = std::pair<api::Term, std::string>();
this->Parser::reset();
if( !strictModeEnabled() ) {
@@ -645,8 +629,8 @@ Smt2::SynthFunFactory::SynthFunFactory(
Smt2* smt2,
const std::string& fun,
bool isInv,
- Type range,
- std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames)
+ api::Sort range,
+ std::vector<std::pair<std::string, api::Sort>>& sortedVarNames)
: d_smt2(smt2), d_fun(fun), d_isInv(isInv)
{
if (range.isNull())
@@ -657,38 +641,37 @@ Smt2::SynthFunFactory::SynthFunFactory(
{
smt2->parseError("Cannot use synth-fun with function return type.");
}
- std::vector<Type> varSorts;
- for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
+ std::vector<api::Sort> varSorts;
+ for (const std::pair<std::string, api::Sort>& p : sortedVarNames)
{
varSorts.push_back(p.second);
}
Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
- Type synthFunType =
- varSorts.size() > 0
- ? d_smt2->getExprManager()->mkFunctionType(varSorts, range)
- : range;
+ api::Sort synthFunType =
+ varSorts.size() > 0 ? d_smt2->getSolver()->mkFunctionSort(varSorts, range)
+ : range;
// we do not allow overloading for synth fun
- d_synthFun = d_smt2->mkBoundVar(fun, synthFunType);
+ d_synthFun = d_smt2->bindBoundVar(fun, synthFunType);
// set the sygus type to be range by default, which is overwritten below
// if a grammar is provided
d_sygusType = range;
d_smt2->pushScope(true);
- d_sygusVars = d_smt2->mkBoundVars(sortedVarNames);
+ d_sygusVars = d_smt2->bindBoundVars(sortedVarNames);
}
Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
-std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(Type grammar)
+std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Sort grammar)
{
Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
- return std::unique_ptr<Command>(
- new SynthFunCommand(d_fun,
- d_synthFun,
- grammar.isNull() ? d_sygusType : grammar,
- d_isInv,
- d_sygusVars));
+ return std::unique_ptr<Command>(new SynthFunCommand(
+ d_fun,
+ d_synthFun.getExpr(),
+ grammar.isNull() ? d_sygusType.getType() : grammar.getType(),
+ d_isInv,
+ api::termVectorToExprs(d_sygusVars)));
}
std::unique_ptr<Command> Smt2::invConstraint(
@@ -705,7 +688,7 @@ std::unique_ptr<Command> Smt2::invConstraint(
"arguments.");
}
- std::vector<Expr> terms;
+ std::vector<api::Term> terms;
for (const std::string& name : names)
{
if (!isDeclared(name))
@@ -718,7 +701,8 @@ std::unique_ptr<Command> Smt2::invConstraint(
terms.push_back(getVariable(name));
}
- return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms));
+ return std::unique_ptr<Command>(
+ new SygusInvConstraintCommand(api::termVectorToExprs(terms)));
}
Command* Smt2::setLogic(std::string name, bool fromCommand)
@@ -932,33 +916,32 @@ void Smt2::includeFile(const std::string& filename) {
parseError("Couldn't open include file `" + path + "'");
}
}
-
bool Smt2::isAbstractValue(const std::string& name)
{
return name.length() >= 2 && name[0] == '@' && name[1] != '0'
&& name.find_first_not_of("0123456789", 1) == std::string::npos;
}
-Expr Smt2::mkAbstractValue(const std::string& name)
+api::Term Smt2::mkAbstractValue(const std::string& name)
{
assert(isAbstractValue(name));
// remove the '@'
- return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
+ return d_solver->mkAbstractValue(name.substr(1));
}
-void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
+void Smt2::mkSygusConstantsForType(const api::Sort& type,
+ std::vector<api::Term>& ops)
+{
if( type.isInteger() ){
- ops.push_back(getExprManager()->mkConst(Rational(0)));
- ops.push_back(getExprManager()->mkConst(Rational(1)));
+ ops.push_back(d_solver->mkReal(0));
+ ops.push_back(d_solver->mkReal(1));
}else if( type.isBitVector() ){
- unsigned sz = ((BitVectorType)type).getSize();
- BitVector bval0(sz, (unsigned int)0);
- ops.push_back( getExprManager()->mkConst(bval0) );
- BitVector bval1(sz, (unsigned int)1);
- ops.push_back( getExprManager()->mkConst(bval1) );
+ uint32_t sz = type.getBVSize();
+ ops.push_back(d_solver->mkBitVector(sz, 0));
+ ops.push_back(d_solver->mkBitVector(sz, 1));
}else if( type.isBoolean() ){
- ops.push_back(getExprManager()->mkConst(true));
- ops.push_back(getExprManager()->mkConst(false));
+ ops.push_back(d_solver->mkTrue());
+ ops.push_back(d_solver->mkFalse());
}
//TODO : others?
}
@@ -969,36 +952,37 @@ void Smt2::processSygusGTerm(
CVC4::SygusGTerm& sgt,
int index,
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops,
std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<std::vector<std::vector<api::Sort>>>& cargs,
std::vector<bool>& allow_const,
std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- const std::vector<CVC4::Expr>& sygus_vars,
- std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
- std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
- CVC4::Type& ret,
+ const std::vector<api::Term>& sygus_vars,
+ std::map<api::Sort, api::Sort>& sygus_to_builtin,
+ std::map<api::Sort, api::Term>& sygus_to_builtin_expr,
+ api::Sort& ret,
bool isNested)
{
if (sgt.d_gterm_type == SygusGTerm::gterm_op)
{
Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype "
<< index << std::endl;
- Kind oldKind;
- Kind newKind = kind::UNDEFINED_KIND;
+ api::Kind oldKind;
+ api::Kind newKind = api::UNDEFINED_KIND;
//convert to UMINUS if one child of MINUS
- if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == kind::MINUS)
+ if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == api::MINUS)
{
- oldKind = kind::MINUS;
- newKind = kind::UMINUS;
+ oldKind = api::MINUS;
+ newKind = api::UMINUS;
}
- if( newKind!=kind::UNDEFINED_KIND ){
+ if (newKind != api::UNDEFINED_KIND)
+ {
Debug("parser-sygus")
<< "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl;
sgt.d_op.d_kind = newKind;
- std::string oldName = kind::kindToString(oldKind);
- std::string newName = kind::kindToString(newKind);
+ std::string oldName = api::kindToString(oldKind);
+ std::string newName = api::kindToString(newKind);
size_t pos = 0;
if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
sgt.d_name.replace(pos, oldName.length(), newName);
@@ -1006,22 +990,32 @@ void Smt2::processSygusGTerm(
}
ops[index].push_back(sgt.d_op);
cnames[index].push_back( sgt.d_name );
- cargs[index].push_back( std::vector< CVC4::Type >() );
+ cargs[index].push_back(std::vector<api::Sort>());
for( unsigned i=0; i<sgt.d_children.size(); i++ ){
std::stringstream ss;
ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
std::string sub_dname = ss.str();
//add datatype for child
- Type null_type;
+ api::Sort null_type;
pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
int sub_dt_index = datatypes.size()-1;
//process child
- Type sub_ret;
+ api::Sort sub_ret;
processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
//process the nested gterm (either pop the last datatype, or flatten the argument)
- Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
- sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
+ api::Sort tt = processSygusNestedGTerm(sub_dt_index,
+ sub_dname,
+ datatypes,
+ sorts,
+ ops,
+ cnames,
+ cargs,
+ allow_const,
+ unresolved_gterm_sym,
+ sygus_to_builtin,
+ sygus_to_builtin_expr,
+ sub_ret);
cargs[index].back().push_back(tt);
}
}
@@ -1030,7 +1024,7 @@ void Smt2::processSygusGTerm(
if( sgt.getNumChildren()!=0 ){
parseError("Bad syntax for Sygus Constant.");
}
- std::vector< Expr > consts;
+ std::vector<api::Term> consts;
mkSygusConstantsForType( sgt.d_type, consts );
Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
for( unsigned i=0; i<consts.size(); i++ ){
@@ -1041,7 +1035,7 @@ void Smt2::processSygusGTerm(
constOp.d_expr = consts[i];
ops[index].push_back(constOp);
cnames[index].push_back( ss.str() );
- cargs[index].push_back( std::vector< CVC4::Type >() );
+ cargs[index].push_back(std::vector<api::Sort>());
}
allow_const[index] = true;
}
@@ -1053,7 +1047,8 @@ void Smt2::processSygusGTerm(
}
Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
for( unsigned i=0; i<sygus_vars.size(); i++ ){
- if( sygus_vars[i].getType()==sgt.d_type ){
+ if (sygus_vars[i].getSort() == sgt.d_type)
+ {
std::stringstream ss;
ss << sygus_vars[i];
Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
@@ -1061,7 +1056,7 @@ void Smt2::processSygusGTerm(
varOp.d_expr = sygus_vars[i];
ops[index].push_back(varOp);
cnames[index].push_back( ss.str() );
- cargs[index].push_back( std::vector< CVC4::Type >() );
+ cargs[index].push_back(std::vector<api::Sort>());
}
}
}
@@ -1092,13 +1087,13 @@ void Smt2::processSygusGTerm(
}
bool Smt2::pushSygusDatatypeDef(
- Type t,
+ api::Sort t,
std::string& dname,
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops,
std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<std::vector<std::vector<api::Sort>>>& cargs,
std::vector<bool>& allow_const,
std::vector<std::vector<std::string>>& unresolved_gterm_sym)
{
@@ -1106,7 +1101,7 @@ bool Smt2::pushSygusDatatypeDef(
datatypes.push_back(Datatype(getExprManager(), dname));
ops.push_back(std::vector<ParseOp>());
cnames.push_back(std::vector<std::string>());
- cargs.push_back(std::vector<std::vector<CVC4::Type> >());
+ cargs.push_back(std::vector<std::vector<api::Sort>>());
allow_const.push_back(false);
unresolved_gterm_sym.push_back(std::vector< std::string >());
return true;
@@ -1114,10 +1109,10 @@ bool Smt2::pushSygusDatatypeDef(
bool Smt2::popSygusDatatypeDef(
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops,
std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<std::vector<std::vector<api::Sort>>>& cargs,
std::vector<bool>& allow_const,
std::vector<std::vector<std::string>>& unresolved_gterm_sym)
{
@@ -1131,21 +1126,21 @@ bool Smt2::popSygusDatatypeDef(
return true;
}
-Type Smt2::processSygusNestedGTerm(
+api::Sort Smt2::processSygusNestedGTerm(
int sub_dt_index,
std::string& sub_dname,
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops,
std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<std::vector<std::vector<api::Sort>>>& cargs,
std::vector<bool>& allow_const,
std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
- std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
- Type sub_ret)
+ std::map<api::Sort, api::Sort>& sygus_to_builtin,
+ std::map<api::Sort, CVC4::api::Term>& sygus_to_builtin_expr,
+ api::Sort sub_ret)
{
- Type t = sub_ret;
+ api::Sort t = sub_ret;
Debug("parser-sygus") << "Argument is ";
if( t.isNull() ){
//then, it is the datatype we constructed, which should have a single constructor
@@ -1156,13 +1151,16 @@ Type Smt2::processSygusNestedGTerm(
parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
}
ParseOp op = ops[sub_dt_index][0];
- Type curr_t;
+ api::Sort curr_t;
if (!op.d_expr.isNull()
&& (op.d_expr.isConst() || cargs[sub_dt_index][0].empty()))
{
- Expr sop = op.d_expr;
- curr_t = sop.getType();
- Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl;
+ api::Term sop = op.d_expr;
+ curr_t = sop.getSort();
+ Debug("parser-sygus")
+ << ": it is constant/0-arg cons " << sop << " with type "
+ << sop.getSort() << ", debug=" << sop.isConst() << " "
+ << cargs[sub_dt_index][0].size() << std::endl;
// only cache if it is a singleton datatype (has unique expr)
if (ops[sub_dt_index].size() == 1)
{
@@ -1176,24 +1174,29 @@ Type Smt2::processSygusNestedGTerm(
}
else
{
- std::vector< Expr > children;
+ std::vector<api::Term> children;
for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
- std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
+ std::map<api::Sort, CVC4::api::Term>::iterator it =
+ sygus_to_builtin_expr.find(cargs[sub_dt_index][0][i]);
if( it==sygus_to_builtin_expr.end() ){
if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
std::stringstream ss;
ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
ss << "Builtin types are currently : " << std::endl;
- for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
+ for (std::map<api::Sort, api::Sort>::iterator itb =
+ sygus_to_builtin.begin();
+ itb != sygus_to_builtin.end();
+ ++itb)
+ {
ss << " " << itb->first << " -> " << itb->second << std::endl;
}
parseError(ss.str());
}
- Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
+ api::Sort bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
std::stringstream ss;
ss << t << "_x_" << i;
- Expr bv = mkBoundVar(ss.str(), bt);
+ api::Term bv = bindBoundVar(ss.str(), bt);
children.push_back( bv );
d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
}else{
@@ -1201,9 +1204,10 @@ Type Smt2::processSygusNestedGTerm(
children.push_back( it->second );
}
}
- Expr e = applyParseOp(op, children);
- Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
- curr_t = e.getType();
+ api::Term e = applyParseOp(op, children);
+ Debug("parser-sygus") << ": constructed " << e << ", which has type "
+ << e.getSort() << std::endl;
+ curr_t = e.getSort();
sygus_to_builtin_expr[t] = e;
}
sorts[sub_dt_index] = curr_t;
@@ -1221,12 +1225,12 @@ Type Smt2::processSygusNestedGTerm(
void Smt2::setSygusStartIndex(const std::string& fun,
int startIndex,
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops)
{
if( startIndex>0 ){
CVC4::Datatype tmp_dt = datatypes[0];
- Type tmp_sort = sorts[0];
+ api::Sort tmp_sort = sorts[0];
std::vector<ParseOp> tmp_ops;
tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
datatypes[0] = datatypes[startIndex];
@@ -1247,9 +1251,9 @@ void Smt2::setSygusStartIndex(const std::string& fun,
void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
std::vector<ParseOp>& ops,
std::vector<std::string>& cnames,
- std::vector<std::vector<CVC4::Type>>& cargs,
+ std::vector<std::vector<api::Sort>>& cargs,
std::vector<std::string>& unresolved_gterm_sym,
- std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin)
+ std::map<api::Sort, api::Sort>& sygus_to_builtin)
{
Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
Debug("parser-sygus") << " add constructors..." << std::endl;
@@ -1295,28 +1299,29 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
<< std::endl;
// make into define-fun
- std::vector<Type> ltypes;
+ std::vector<api::Sort> ltypes;
for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
{
ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
}
- std::vector<Expr> largs;
- Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
+ std::vector<api::Term> largs;
+ api::Term lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
// make the let_body
- Expr body = applyParseOp(ops[i], largs);
+ api::Term body = applyParseOp(ops[i], largs);
// replace by lambda
ParseOp pLam;
- pLam.d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+ pLam.d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body);
ops[i] = pLam;
Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl;
// callback prints as the expression
- spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
+ spc = std::make_shared<printer::SygusExprPrintCallback>(
+ body.getExpr(), api::termVectorToExprs(largs));
}
else
{
- Expr sop = ops[i].d_expr;
- if (!sop.isNull() && sop.getType().isBitVector() && sop.isConst())
+ api::Term sop = ops[i].d_expr;
+ if (!sop.isNull() && sop.getSort().isBitVector() && sop.isConst())
{
Debug("parser-sygus") << "--> Bit-vector constant " << sop << " ("
<< cnames[i] << ")" << std::endl;
@@ -1326,22 +1331,22 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
// the given name.
spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
}
- else if (!sop.isNull() && sop.getKind() == kind::VARIABLE)
+ else if (!sop.isNull() && sop.getKind() == api::VARIABLE)
{
Debug("parser-sygus") << "--> Defined function " << ops[i]
<< std::endl;
// turn f into (lammbda (x) (f x))
// in a degenerate case, ops[i] may be a defined constant,
// in which case we do not replace by a lambda.
- if (sop.getType().isFunction())
+ if (sop.getSort().isFunction())
{
- std::vector<Type> ftypes =
- static_cast<FunctionType>(sop.getType()).getArgTypes();
- std::vector<Expr> largs;
- Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
+ std::vector<api::Sort> ftypes =
+ sop.getSort().getFunctionDomainSorts();
+ std::vector<api::Term> largs;
+ api::Term lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
largs.insert(largs.begin(), sop);
- Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
- ops[i].d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+ api::Term body = d_solver->mkTerm(api::APPLY_UF, largs);
+ ops[i].d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body);
Debug("parser-sygus") << " ...replace op : " << ops[i]
<< std::endl;
}
@@ -1364,15 +1369,22 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
cnames[i] = ss.str();
Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..."
<< std::endl;
+
// Add the sygus constructor, either using the expression operator of
// ops[i], or the kind.
if (!ops[i].d_expr.isNull())
{
- dt.addSygusConstructor(ops[i].d_expr, cnames[i], cargs[i], spc);
+ dt.addSygusConstructor(ops[i].d_expr.getExpr(),
+ cnames[i],
+ api::sortVectorToTypes(cargs[i]),
+ spc);
}
- else if (ops[i].d_kind != kind::NULL_EXPR)
+ else if (ops[i].d_kind != api::NULL_EXPR)
{
- dt.addSygusConstructor(ops[i].d_kind, cnames[i], cargs[i], spc);
+ dt.addSygusConstructor(extToIntKind(ops[i].d_kind),
+ cnames[i],
+ api::sortVectorToTypes(cargs[i]),
+ spc);
}
else
{
@@ -1387,36 +1399,38 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl;
if( !unresolved_gterm_sym.empty() ){
- std::vector< Type > types;
+ std::vector<api::Sort> types;
Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym[i] << std::endl;
if( isUnresolvedType(unresolved_gterm_sym[i]) ){
Debug("parser-sygus") << " it is an unresolved type." << std::endl;
- Type t = getSort(unresolved_gterm_sym[i]);
+ api::Sort t = getSort(unresolved_gterm_sym[i]);
if( std::find( types.begin(), types.end(), t )==types.end() ){
types.push_back( t );
//identity element
- Type bt = dt.getSygusType();
+ api::Sort bt = dt.getSygusType();
Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl;
std::stringstream ss;
ss << t << "_x";
- Expr var = mkBoundVar(ss.str(), bt);
- std::vector<Expr> lchildren;
- lchildren.push_back(
- getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
+ api::Term var = bindBoundVar(ss.str(), bt);
+ std::vector<api::Term> lchildren;
+ lchildren.push_back(d_solver->mkTerm(api::BOUND_VAR_LIST, var));
lchildren.push_back(var);
- Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren);
+ api::Term id_op = d_solver->mkTerm(api::LAMBDA, lchildren);
// empty sygus callback (should not be printed)
std::shared_ptr<SygusPrintCallback> sepc =
std::make_shared<printer::SygusEmptyPrintCallback>();
//make the sygus argument list
- std::vector< Type > id_carg;
+ std::vector<api::Sort> id_carg;
id_carg.push_back( t );
- dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
+ dt.addSygusConstructor(id_op.getExpr(),
+ unresolved_gterm_sym[i],
+ api::sortVectorToTypes(id_carg),
+ sepc);
//add to operators
ParseOp idOp;
@@ -1432,31 +1446,30 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
}
}
-Expr Smt2::makeSygusBoundVarList(Datatype& dt,
- unsigned i,
- const std::vector<Type>& ltypes,
- std::vector<Expr>& lvars)
+api::Term Smt2::makeSygusBoundVarList(CVC4::Datatype& dt,
+ unsigned i,
+ const std::vector<api::Sort>& ltypes,
+ std::vector<api::Term>& lvars)
{
for (unsigned j = 0, size = ltypes.size(); j < size; j++)
{
std::stringstream ss;
ss << dt.getName() << "_x_" << i << "_" << j;
- Expr v = mkBoundVar(ss.str(), ltypes[j]);
+ api::Term v = bindBoundVar(ss.str(), ltypes[j]);
lvars.push_back(v);
}
- return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
+ return d_solver->mkTerm(api::BOUND_VAR_LIST, lvars);
}
-void Smt2::addSygusConstructorTerm(Datatype& dt,
- Expr term,
- std::map<Expr, Type>& ntsToUnres) const
+void Smt2::addSygusConstructorTerm(
+ Datatype& dt,
+ api::Term term,
+ std::map<api::Term, api::Sort>& ntsToUnres) const
{
Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
- // Ensure that we do type checking here to catch sygus constructors with
- // malformed builtin operators. The argument "true" to getType here forces
- // a recursive well-typedness check.
- term.getType(true);
- // purify each occurrence of a non-terminal symbol in term, replace by
+ // At this point, we should know that dt is well founded, and that its
+ // builtin sygus operators are well-typed.
+ // Now, purify each occurrence of a non-terminal symbol in term, replace by
// free variables. These become arguments to constructors. Notice we must do
// a tree traversal in this function, since unique paths to the same term
// should be treated as distinct terms.
@@ -1464,7 +1477,7 @@ void Smt2::addSygusConstructorTerm(Datatype& dt,
// this does not lead to exponential behavior with respect to input size.
std::vector<api::Term> args;
std::vector<api::Sort> cargs;
- api::Term op = purifySygusGTerm(api::Term(term), ntsToUnres, args, cargs);
+ api::Term op = purifySygusGTerm(term, ntsToUnres, args, cargs);
std::stringstream ssCName;
ssCName << op.getKind();
Trace("parser-sygus2") << "Purified operator " << op
@@ -1487,14 +1500,14 @@ void Smt2::addSygusConstructorTerm(Datatype& dt,
}
api::Term Smt2::purifySygusGTerm(api::Term term,
- std::map<Expr, Type>& ntsToUnres,
+ std::map<api::Term, api::Sort>& ntsToUnres,
std::vector<api::Term>& args,
std::vector<api::Sort>& cargs) const
{
Trace("parser-sygus2-debug")
<< "purifySygusGTerm: " << term
<< " #nchild=" << term.getExpr().getNumChildren() << std::endl;
- std::map<Expr, Type>::iterator itn = ntsToUnres.find(term.getExpr());
+ std::map<api::Term, api::Sort>::iterator itn = ntsToUnres.find(term);
if (itn != ntsToUnres.end())
{
api::Term ret = d_solver->mkVar(term.getSort());
@@ -1526,35 +1539,35 @@ api::Term Smt2::purifySygusGTerm(api::Term term,
}
void Smt2::addSygusConstructorVariables(Datatype& dt,
- const std::vector<Expr>& sygusVars,
- Type type) const
+ const std::vector<api::Term>& sygusVars,
+ api::Sort type) const
{
// each variable of appropriate type becomes a sygus constructor in dt.
for (unsigned i = 0, size = sygusVars.size(); i < size; i++)
{
- Expr v = sygusVars[i];
- if (v.getType() == type)
+ api::Term v = sygusVars[i];
+ if (v.getSort() == type)
{
std::stringstream ss;
ss << v;
- std::vector<CVC4::Type> cargs;
- dt.addSygusConstructor(v, ss.str(), cargs);
+ std::vector<api::Sort> cargs;
+ dt.addSygusConstructor(
+ v.getExpr(), ss.str(), api::sortVectorToTypes(cargs));
}
}
}
InputLanguage Smt2::getLanguage() const
{
- ExprManager* em = getExprManager();
- return em->getOptions().getInputLanguage();
+ return getExprManager()->getOptions().getInputLanguage();
}
-void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type)
+void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
{
Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
<< std::endl;
// (as const (Array T1 T2))
- if (p.d_kind == kind::STORE_ALL)
+ if (p.d_kind == api::STORE_ALL)
{
if (!type.isArray())
{
@@ -1576,6 +1589,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type)
if (isDeclared(p.d_name, SYM_VARIABLE))
{
p.d_expr = getExpressionForNameAndType(p.d_name, type);
+ p.d_name = std::string("");
}
if (p.d_expr.isNull())
{
@@ -1586,17 +1600,18 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type)
}
}
Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
- Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getType();
+ Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort();
Trace("parser-qid") << std::endl;
// otherwise, we process the type ascription
p.d_expr =
applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr();
}
-Expr Smt2::parseOpToExpr(ParseOp& p)
+api::Term Smt2::parseOpToExpr(ParseOp& p)
{
- Expr expr;
- if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull())
+ Debug("parser") << "parseOpToExpr: " << p << std::endl;
+ api::Term expr;
+ if (p.d_kind != api::NULL_EXPR || !p.d_type.isNull())
{
parseError(
"Bad syntax for qualified identifier operator in term position.");
@@ -1611,7 +1626,7 @@ Expr Smt2::parseOpToExpr(ParseOp& p)
&& p.d_name.find_first_not_of("0123456789", 1) == std::string::npos)
{
// allow unary minus in sygus version 1
- expr = getExprManager()->mkConst(Rational(p.d_name));
+ expr = d_solver->mkReal(p.d_name);
}
else
{
@@ -1628,38 +1643,41 @@ Expr Smt2::parseOpToExpr(ParseOp& p)
return expr;
}
-Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
+api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
{
bool isBuiltinOperator = false;
// the builtin kind of the overall return expression
- Kind kind = kind::NULL_EXPR;
+ api::Kind kind = api::NULL_EXPR;
// First phase: process the operator
if (Debug.isOn("parser"))
{
Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
- for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+ for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
+ ++i)
{
Debug("parser") << "++ " << *i << std::endl;
}
}
api::Op op;
- if (p.d_kind != kind::NULL_EXPR)
+ if (p.d_kind != api::NULL_EXPR)
{
// It is a special case, e.g. tupSel or array constant specification.
// We have to wait until the arguments are parsed to resolve it.
}
else if (!p.d_expr.isNull())
{
- // An explicit operator, e.g. an indexed symbol.
- args.insert(args.begin(), p.d_expr);
- Kind fkind = getKindForFunction(p.d_expr);
- if (fkind != kind::UNDEFINED_KIND)
+ // An explicit operator, e.g. an apply function
+ api::Kind fkind = getKindForFunction(p.d_expr);
+ if (fkind != api::UNDEFINED_KIND)
{
// Some operators may require a specific kind.
// Testers are handled differently than other indexed operators,
// since they require a kind.
kind = fkind;
+ Debug("parser") << "Got function kind " << kind << " for expression "
+ << std::endl;
}
+ args.insert(args.begin(), p.d_expr);
}
else if (!p.d_op.isNull())
{
@@ -1678,7 +1696,7 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
{
// A non-built-in function application, get the expression
checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
- Expr v = getVariable(p.d_name);
+ api::Term v = getVariable(p.d_name);
if (!v.isNull())
{
checkFunctionLike(v);
@@ -1691,12 +1709,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
// Could not find the expression. It may be an overloaded symbol,
// in which case we may find it after knowing the types of its
// arguments.
- std::vector<Type> argTypes;
- for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+ std::vector<api::Sort> argTypes;
+ for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
+ ++i)
{
- argTypes.push_back((*i).getType());
+ argTypes.push_back((*i).getSort());
}
- Expr fop = getOverloadedFunctionForTypes(p.d_name, argTypes);
+ api::Term fop = getOverloadedFunctionForTypes(p.d_name, argTypes);
if (!fop.isNull())
{
checkFunctionLike(fop);
@@ -1715,13 +1734,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
// Second phase: apply the arguments to the parse op
ExprManager* em = getExprManager();
// handle special cases
- if (p.d_kind == kind::STORE_ALL && !p.d_type.isNull())
+ if (p.d_kind == api::STORE_ALL && !p.d_type.isNull())
{
if (args.size() != 1)
{
parseError("Too many arguments to array constant.");
}
- Expr constVal = args[0];
+ api::Term constVal = args[0];
if (!constVal.isConst())
{
// To parse array constants taking reals whose values are specified by
@@ -1732,12 +1751,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
// like 5.0 which are converted to (/ 5 1) to distinguish them from
// integer constants. We must ensure numerator and denominator are
// constant and the denominator is non-zero.
- if (constVal.getKind() == kind::DIVISION && constVal[0].isConst()
+ if (constVal.getKind() == api::DIVISION && constVal[0].isConst()
&& constVal[1].isConst()
- && !constVal[1].getConst<Rational>().isZero())
+ && !constVal[1].getExpr().getConst<Rational>().isZero())
{
- constVal = em->mkConst(constVal[0].getConst<Rational>()
- / constVal[1].getConst<Rational>());
+ std::stringstream sdiv;
+ sdiv << constVal[0] << "/" << constVal[1];
+ constVal = d_solver->mkReal(sdiv.str());
}
if (!constVal.isConst())
{
@@ -1748,47 +1768,52 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
parseError(ss.str());
}
}
- ArrayType aqtype = static_cast<ArrayType>(p.d_type);
- if (!aqtype.getConstituentType().isComparableTo(constVal.getType()))
+ if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
{
std::stringstream ss;
ss << "type mismatch inside array constant term:" << std::endl
<< "array type: " << p.d_type << std::endl
- << "expected const type: " << aqtype.getConstituentType() << std::endl
- << "computed const type: " << constVal.getType();
+ << "expected const type: " << p.d_type.getArrayElementSort()
+ << std::endl
+ << "computed const type: " << constVal.getSort();
parseError(ss.str());
}
- return em->mkConst(ArrayStoreAll(p.d_type, constVal));
+ api::Term ret = d_solver->mkConstArray(p.d_type, constVal);
+ Debug("parser") << "applyParseOp: return store all " << ret << std::endl;
+ return ret;
}
- else if (p.d_kind == kind::APPLY_SELECTOR && !p.d_expr.isNull())
+ else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
{
// tuple selector case
- Integer x = p.d_expr.getConst<Rational>().getNumerator();
+ Integer x = p.d_expr.getExpr().getConst<Rational>().getNumerator();
if (!x.fitsUnsignedInt())
{
parseError("index of tupSel is larger than size of unsigned int");
}
unsigned int n = x.toUnsignedInt();
- if (args.size() > 1)
+ if (args.size() != 1)
{
- parseError("tupSel applied to more than one tuple argument");
+ parseError("tupSel should only be applied to one tuple argument");
}
- Type t = args[0].getType();
+ api::Sort t = args[0].getSort();
if (!t.isTuple())
{
parseError("tupSel applied to non-tuple");
}
- size_t length = ((DatatypeType)t).getTupleLength();
+ size_t length = t.getTupleLength();
if (n >= length)
{
std::stringstream ss;
ss << "tuple is of length " << length << "; cannot access index " << n;
parseError(ss.str());
}
- const Datatype& dt = ((DatatypeType)t).getDatatype();
- return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args);
+ const Datatype& dt = ((DatatypeType)t.getType()).getDatatype();
+ api::Term ret = d_solver->mkTerm(
+ api::APPLY_SELECTOR, api::Term(dt[0][n].getSelector()), args[0]);
+ Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
+ return ret;
}
- else if (p.d_kind != kind::NULL_EXPR)
+ else if (p.d_kind != api::NULL_EXPR)
{
// it should not have an expression or type specified at this point
if (!p.d_expr.isNull() || !p.d_type.isNull())
@@ -1802,43 +1827,47 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
}
else if (isBuiltinOperator)
{
+ Trace("ajr-temp") << "mkTerm builtin operator" << std::endl;
if (!em->getOptions().getUfHo()
- && (kind == kind::EQUAL || kind == kind::DISTINCT))
+ && (kind == api::EQUAL || kind == api::DISTINCT))
{
// need --uf-ho if these operators are applied over function args
- for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+ for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
+ ++i)
{
- if ((*i).getType().isFunction())
+ if ((*i).getSort().isFunction())
{
parseError(
"Cannot apply equalty to functions unless --uf-ho is set.");
}
}
}
- if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
+ if (!strictModeEnabled() && (kind == api::AND || kind == api::OR)
&& args.size() == 1)
{
// Unary AND/OR can be replaced with the argument.
+ Debug("parser") << "applyParseOp: return unary " << args[0] << std::endl;
return args[0];
}
- else if (kind == kind::MINUS && args.size() == 1)
+ else if (kind == api::MINUS && args.size() == 1)
{
- return em->mkExpr(kind::UMINUS, args[0]);
+ api::Term ret = d_solver->mkTerm(api::UMINUS, args[0]);
+ Debug("parser") << "applyParseOp: return uminus " << ret << std::endl;
+ return ret;
}
- api::Term ret =
- d_solver->mkTerm(intToExtKind(kind), api::exprVectorToTerms(args));
+ api::Term ret = d_solver->mkTerm(kind, args);
Debug("parser") << "applyParseOp: return default builtin " << ret
<< std::endl;
- return ret.getExpr();
+ return ret;
}
if (args.size() >= 2)
{
// may be partially applied function, in this case we use HO_APPLY
- Type argt = args[0].getType();
+ api::Sort argt = args[0].getSort();
if (argt.isFunction())
{
- unsigned arity = static_cast<FunctionType>(argt).getArity();
+ unsigned arity = argt.getFunctionArity();
if (args.size() - 1 < arity)
{
if (!em->getOptions().getUfHo())
@@ -1848,26 +1877,33 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
Debug("parser") << "Partial application of " << args[0];
Debug("parser") << " : #argTypes = " << arity;
Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
+ api::Term ret = d_solver->mkTerm(api::HO_APPLY, args);
+ Debug("parser") << "applyParseOp: return curry higher order " << ret
+ << std::endl;
// must curry the partial application
- return em->mkLeftAssociative(kind::HO_APPLY, args);
+ return ret;
}
}
}
if (!op.isNull())
{
- api::Term ret = d_solver->mkTerm(op, api::exprVectorToTerms(args));
+ api::Term ret = d_solver->mkTerm(op, args);
Debug("parser") << "applyParseOp: return op : " << ret << std::endl;
- return ret.getExpr();
+ return ret;
}
- if (kind == kind::NULL_EXPR)
+ if (kind == api::NULL_EXPR)
{
- std::vector<Expr> eargs(args.begin() + 1, args.end());
- return em->mkExpr(args[0], eargs);
- }
- return em->mkExpr(kind, args);
+ // should never happen in the new API
+ parseError("do not know how to process parse op");
+ }
+ Debug("parser") << "Try default term construction for kind " << kind
+ << " #args = " << args.size() << "..." << std::endl;
+ api::Term ret = d_solver->mkTerm(kind, args);
+ Debug("parser") << "applyParseOp: return : " << ret << std::endl;
+ return ret;
}
-Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
+api::Term Smt2::setNamedAttribute(api::Term& expr, const SExpr& sexpr)
{
if (!sexpr.isKeyword())
{
@@ -1876,7 +1912,7 @@ Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
std::string name = sexpr.getValue();
checkUserSymbol(name);
// ensure expr is a closed subterm
- if (expr.hasFreeVariable())
+ if (expr.getExpr().hasFreeVariable())
{
std::stringstream ss;
ss << ":named annotations can only name terms that are closed";
@@ -1885,19 +1921,17 @@ Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
// check that sexpr is a fresh function symbol, and reserve it
reserveSymbolAtAssertionLevel(name);
// define it
- Expr func = mkVar(name, expr.getType(), ExprManager::VAR_FLAG_DEFINED);
+ api::Term func = bindVar(name, expr.getSort(), ExprManager::VAR_FLAG_DEFINED);
// remember the last term to have been given a :named attribute
setLastNamedTerm(expr, name);
return func;
}
-Expr Smt2::mkAnd(const std::vector<Expr>& es)
+api::Term Smt2::mkAnd(const std::vector<api::Term>& es)
{
- ExprManager* em = getExprManager();
-
if (es.size() == 0)
{
- return em->mkConst(true);
+ return d_solver->mkTrue();
}
else if (es.size() == 1)
{
@@ -1905,7 +1939,7 @@ Expr Smt2::mkAnd(const std::vector<Expr>& es)
}
else
{
- return em->mkExpr(kind::AND, es);
+ return d_solver->mkTerm(api::AND, es);
}
}
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 53ebf5929..afa60bf2f 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -72,15 +72,15 @@ class Smt2 : public Parser
bool d_seenSetLogic;
LogicInfo d_logic;
- std::unordered_map<std::string, Kind> operatorKindMap;
+ std::unordered_map<std::string, api::Kind> operatorKindMap;
/**
* Maps indexed symbols to the kind of the operator (e.g. "extract" to
* BITVECTOR_EXTRACT).
*/
std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
- std::pair<Expr, std::string> d_lastNamedTerm;
+ std::pair<api::Term, std::string> d_lastNamedTerm;
// for sygus
- std::vector<Expr> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints,
+ std::vector<api::Term> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints,
d_sygusFunSymbols;
protected:
@@ -97,7 +97,7 @@ class Smt2 : public Parser
*/
void addTheory(Theory theory);
- void addOperator(Kind k, const std::string& name);
+ void addOperator(api::Kind k, const std::string& name);
/**
* Registers an indexed function symbol.
@@ -109,11 +109,11 @@ class Smt2 : public Parser
* @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT)
* @param name The name of the symbol (e.g. "extract")
*/
- void addIndexedOperator(Kind tKind,
+ void addIndexedOperator(api::Kind tKind,
api::Kind opKind,
const std::string& name);
- Kind getOperatorKind(const std::string& name) const;
+ api::Kind getOperatorKind(const std::string& name) const;
bool isOperatorEnabled(const std::string& name) const;
@@ -147,7 +147,8 @@ class Smt2 : public Parser
/**
* Returns the expression that name should be interpreted as.
*/
- Expr getExpressionForNameAndType(const std::string& name, Type t) override;
+ api::Term getExpressionForNameAndType(const std::string& name,
+ api::Sort t) override;
/** Make function defined by a define-fun(s)-rec command.
*
@@ -163,11 +164,11 @@ class Smt2 : public Parser
* added to flattenVars in this function if the function is given a function
* range type.
*/
- Expr mkDefineFunRec(
+ api::Term bindDefineFunRec(
const std::string& fname,
- const std::vector<std::pair<std::string, Type> >& sortedVarNames,
- Type t,
- std::vector<Expr>& flattenVars);
+ const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
+ api::Sort t,
+ std::vector<api::Term>& flattenVars);
/** Push scope for define-fun-rec
*
@@ -187,10 +188,10 @@ class Smt2 : public Parser
* that defined this definition and stores it in bvs.
*/
void pushDefineFunRecScope(
- const std::vector<std::pair<std::string, Type> >& sortedVarNames,
- Expr func,
- const std::vector<Expr>& flattenVars,
- std::vector<Expr>& bvs,
+ const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
+ api::Term func,
+ const std::vector<api::Term>& flattenVars,
+ std::vector<api::Term>& bvs,
bool bindingLevel = false);
void reset() override;
@@ -218,11 +219,11 @@ class Smt2 : public Parser
Smt2* smt2,
const std::string& fun,
bool isInv,
- Type range,
- std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames);
+ api::Sort range,
+ std::vector<std::pair<std::string, api::Sort>>& sortedVarNames);
~SynthFunFactory();
- const std::vector<Expr>& getSygusVars() const { return d_sygusVars; }
+ const std::vector<api::Term>& getSygusVars() const { return d_sygusVars; }
/**
* Create an instance of `SynthFunCommand`.
@@ -230,15 +231,15 @@ class Smt2 : public Parser
* @param grammar Optional grammar associated with the synth-fun command
* @return The instance of `SynthFunCommand`
*/
- std::unique_ptr<Command> mkCommand(Type grammar);
+ std::unique_ptr<Command> mkCommand(api::Sort grammar);
private:
Smt2* d_smt2;
std::string d_fun;
- Expr d_synthFun;
- Type d_sygusType;
+ api::Term d_synthFun;
+ api::Sort d_sygusType;
bool d_isInv;
- std::vector<Expr> d_sygusVars;
+ std::vector<api::Term> d_sygusVars;
};
/**
@@ -321,17 +322,16 @@ class Smt2 : public Parser
void includeFile(const std::string& filename);
- void setLastNamedTerm(Expr e, std::string name) {
+ void setLastNamedTerm(api::Term e, std::string name)
+ {
d_lastNamedTerm = std::make_pair(e, name);
}
void clearLastNamedTerm() {
- d_lastNamedTerm = std::make_pair(Expr(), "");
+ d_lastNamedTerm = std::make_pair(api::Term(), "");
}
- std::pair<Expr, std::string> lastNamedTerm() {
- return d_lastNamedTerm;
- }
+ std::pair<api::Term, std::string> lastNamedTerm() { return d_lastNamedTerm; }
/** Does name denote an abstract value? (of the form '@n' for numeral n). */
bool isAbstractValue(const std::string& name);
@@ -341,58 +341,59 @@ class Smt2 : public Parser
* Abstract values are used for processing get-value calls. The argument
* name should be such that isAbstractValue(name) is true.
*/
- Expr mkAbstractValue(const std::string& name);
+ api::Term mkAbstractValue(const std::string& name);
- void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
+ void mkSygusConstantsForType(const api::Sort& type,
+ std::vector<api::Term>& ops);
void processSygusGTerm(
CVC4::SygusGTerm& sgt,
int index,
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops,
std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<std::vector<std::vector<api::Sort>>>& cargs,
std::vector<bool>& allow_const,
std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- const std::vector<CVC4::Expr>& sygus_vars,
- std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
- std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
- CVC4::Type& ret,
+ const std::vector<api::Term>& sygus_vars,
+ std::map<api::Sort, api::Sort>& sygus_to_builtin,
+ std::map<api::Sort, api::Term>& sygus_to_builtin_expr,
+ api::Sort& ret,
bool isNested = false);
bool pushSygusDatatypeDef(
- Type t,
+ api::Sort t,
std::string& dname,
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops,
std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<std::vector<std::vector<api::Sort>>>& cargs,
std::vector<bool>& allow_const,
std::vector<std::vector<std::string>>& unresolved_gterm_sym);
bool popSygusDatatypeDef(
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops,
std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<std::vector<std::vector<api::Sort>>>& cargs,
std::vector<bool>& allow_const,
std::vector<std::vector<std::string>>& unresolved_gterm_sym);
void setSygusStartIndex(const std::string& fun,
int startIndex,
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops);
void mkSygusDatatype(CVC4::Datatype& dt,
std::vector<ParseOp>& ops,
std::vector<std::string>& cnames,
- std::vector<std::vector<CVC4::Type>>& cargs,
+ std::vector<std::vector<api::Sort>>& cargs,
std::vector<std::string>& unresolved_gterm_sym,
- std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin);
+ std::map<api::Sort, api::Sort>& sygus_to_builtin);
/**
* Adds a constructor to sygus datatype dt whose sygus operator is term.
@@ -407,17 +408,18 @@ class Smt2 : public Parser
* with bound variables via purifySygusGTerm, and binding these variables
* via a lambda.
*/
- void addSygusConstructorTerm(Datatype& dt,
- Expr term,
- std::map<Expr, Type>& ntsToUnres) const;
+ void addSygusConstructorTerm(
+ Datatype& dt,
+ api::Term term,
+ std::map<api::Term, api::Sort>& ntsToUnres) const;
/**
* This adds constructors to dt for sygus variables in sygusVars whose
* type is argument type. This method should be called when the sygus grammar
* term (Variable type) is encountered.
*/
void addSygusConstructorVariables(Datatype& dt,
- const std::vector<Expr>& sygusVars,
- Type type) const;
+ const std::vector<api::Term>& sygusVars,
+ api::Sort type) const;
/**
* Smt2 parser provides its own checkDeclaration, which does the
@@ -446,40 +448,6 @@ class Smt2 : public Parser
}
this->Parser::checkDeclaration(name, check, type, notes);
}
-
- void checkOperator(Kind kind, unsigned numArgs)
- {
- Parser::checkOperator(kind, numArgs);
- // strict SMT-LIB mode enables extra checks for some bitvector operators
- // that CVC4 permits as N-ary but the standard requires is binary
- if(strictModeEnabled()) {
- switch(kind) {
- case kind::BITVECTOR_AND:
- case kind::BITVECTOR_MULT:
- case kind::BITVECTOR_OR:
- case kind::BITVECTOR_PLUS:
- case kind::BITVECTOR_XOR:
- if (numArgs != 2 && !v2_6())
- {
- parseError(
- "Operator requires exactly 2 arguments in strict SMT-LIB "
- "compliance mode (for versions <2.6): "
- + kindToString(kind));
- }
- break;
- case kind::BITVECTOR_CONCAT:
- if(numArgs != 2) {
- parseError(
- "Operator requires exactly 2 arguments in strict SMT-LIB "
- "compliance mode: "
- + kindToString(kind));
- }
- break;
- default:
- break; /* no problem */
- }
- }
- }
/** Set named attribute
*
* This is called when expression expr is annotated with a name, i.e.
@@ -490,7 +458,7 @@ class Smt2 : public Parser
* which is used later for tracking assertions in unsat cores. This
* symbol is returned by this method.
*/
- Expr setNamedAttribute(Expr& expr, const SExpr& sexpr);
+ api::Term setNamedAttribute(api::Term& expr, const SExpr& sexpr);
// Throw a ParserException with msg appended with the current logic.
inline void parseErrorLogic(const std::string& msg)
@@ -516,7 +484,7 @@ class Smt2 : public Parser
* - If p's expression field is set, then we leave p unchanged, check if
* that expression has the given type and throw a parse error otherwise.
*/
- void parseOpApplyTypeAscription(ParseOp& p, Type type);
+ void parseOpApplyTypeAscription(ParseOp& p, api::Sort type);
/**
* This converts a ParseOp to expression, assuming it is a standalone term.
*
@@ -526,7 +494,7 @@ class Smt2 : public Parser
* of this class.
* In other cases, a parse error is thrown.
*/
- Expr parseOpToExpr(ParseOp& p);
+ api::Term parseOpToExpr(ParseOp& p);
/**
* Apply parse operator to list of arguments, and return the resulting
* expression.
@@ -559,24 +527,24 @@ class Smt2 : public Parser
* - If the overall expression is a partial application, then we process this
* as a chain of HO_APPLY terms.
*/
- Expr applyParseOp(ParseOp& p, std::vector<Expr>& args);
+ api::Term applyParseOp(ParseOp& p, std::vector<api::Term>& args);
//------------------------- end processing parse operators
private:
- std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type;
+ std::map<api::Term, api::Sort> d_sygus_bound_var_type;
- Type processSygusNestedGTerm(
+ api::Sort processSygusNestedGTerm(
int sub_dt_index,
std::string& sub_dname,
std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
+ std::vector<api::Sort>& sorts,
std::vector<std::vector<ParseOp>>& ops,
std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<std::vector<std::vector<api::Sort>>>& cargs,
std::vector<bool>& allow_const,
std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
- std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
- Type sub_ret);
+ std::map<api::Sort, api::Sort>& sygus_to_builtin,
+ std::map<api::Sort, api::Term>& sygus_to_builtin_expr,
+ api::Sort sub_ret);
/** make sygus bound var list
*
@@ -586,10 +554,10 @@ class Smt2 : public Parser
* It appends a bound variable to lvars for each type in ltypes, and returns
* a bound variable list whose children are lvars.
*/
- Expr makeSygusBoundVarList(Datatype& dt,
- unsigned i,
- const std::vector<Type>& ltypes,
- std::vector<Expr>& lvars);
+ api::Term makeSygusBoundVarList(CVC4::Datatype& dt,
+ unsigned i,
+ const std::vector<api::Sort>& ltypes,
+ std::vector<api::Term>& lvars);
/** Purify sygus grammar term
*
@@ -603,7 +571,7 @@ class Smt2 : public Parser
* sygus constructor.
*/
api::Term purifySygusGTerm(api::Term term,
- std::map<Expr, Type>& ntsToUnres,
+ std::map<api::Term, api::Sort>& ntsToUnres,
std::vector<api::Term>& args,
std::vector<api::Sort>& cargs) const;
@@ -632,7 +600,7 @@ class Smt2 : public Parser
* @return True if `es` is empty, `e` if `es` consists of a single element
* `e`, the conjunction of expressions otherwise.
*/
- Expr mkAnd(const std::vector<Expr>& es);
+ api::Term mkAnd(const std::vector<api::Term>& es);
}; /* class Smt2 */
}/* CVC4::parser namespace */
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 4e74eefb5..c0bece257 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -64,7 +64,7 @@ Command* Smt2Input::parseCommand() {
api::Term Smt2Input::parseExpr()
{
- return api::Term(d_pSmt2Parser->parseExpr(d_pSmt2Parser));
+ return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
}
}/* CVC4::parser namespace */
diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp
index f0bed978e..a908bf4d5 100644
--- a/src/parser/smt2/sygus_input.cpp
+++ b/src/parser/smt2/sygus_input.cpp
@@ -65,7 +65,7 @@ Command* SygusInput::parseCommand() {
api::Term SygusInput::parseExpr()
{
- return api::Term(d_pSmt2Parser->parseExpr(d_pSmt2Parser));
+ return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
}
}/* CVC4::parser namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback