** Top contributors (to current version):
** Andrew Reynolds, Kshitij Bansal, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**/
#include "parser/smt2/smt2.h"
-
#include "expr/type.h"
+#include "options/options.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/smt1/smt1.h"
#include "parser/smt2/smt2_input.h"
-#include "smt/command.h"
+#include "printer/sygus_print_callback.h"
#include "util/bitvector.h"
#include <algorithm>
namespace CVC4 {
namespace parser {
-Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
- Parser(exprManager,input,strictMode,parseOnly),
- d_logicSet(false) {
- if( !strictModeEnabled() ) {
+Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
+ : Parser(solver, input, strictMode, parseOnly),
+ d_logicSet(false),
+ d_seenSetLogic(false)
+{
+ if (!strictModeEnabled())
+ {
addTheory(Smt2::THEORY_CORE);
}
}
-void Smt2::setLanguage(InputLanguage lang) {
- ((Smt2Input*) getInput())->setLanguage(lang);
-}
-
void Smt2::addArithmeticOperators() {
- Parser::addOperator(kind::PLUS);
- Parser::addOperator(kind::MINUS);
+ addOperator(kind::PLUS, "+");
+ addOperator(kind::MINUS, "-");
+ // kind::MINUS is converted to kind::UMINUS if there is only a single operand
Parser::addOperator(kind::UMINUS);
- Parser::addOperator(kind::MULT);
- Parser::addOperator(kind::LT);
- Parser::addOperator(kind::LEQ);
- Parser::addOperator(kind::GT);
- Parser::addOperator(kind::GEQ);
-
- addOperator(kind::POW, "^");
+ addOperator(kind::MULT, "*");
+ addOperator(kind::LT, "<");
+ addOperator(kind::LEQ, "<=");
+ addOperator(kind::GT, ">");
+ addOperator(kind::GEQ, ">=");
+
+ if (!strictModeEnabled())
+ {
+ // NOTE: this operator is non-standard
+ addOperator(kind::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");
+}
+
+void Smt2::addQuantifiersOperators()
+{
+ if (!strictModeEnabled())
+ {
+ addOperator(kind::INST_CLOSURE, "inst-closure");
+ }
}
void Smt2::addBitvectorOperators() {
addOperator(kind::BITVECTOR_SGE, "bvsge");
addOperator(kind::BITVECTOR_REDOR, "bvredor");
addOperator(kind::BITVECTOR_REDAND, "bvredand");
+ addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
+
+ addIndexedOperator(
+ kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract");
+ addIndexedOperator(
+ kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT_OP, "repeat");
+ addIndexedOperator(kind::BITVECTOR_ZERO_EXTEND,
+ api::BITVECTOR_ZERO_EXTEND_OP,
+ "zero_extend");
+ addIndexedOperator(kind::BITVECTOR_SIGN_EXTEND,
+ api::BITVECTOR_SIGN_EXTEND_OP,
+ "sign_extend");
+ addIndexedOperator(kind::BITVECTOR_ROTATE_LEFT,
+ api::BITVECTOR_ROTATE_LEFT_OP,
+ "rotate_left");
+ addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
+ api::BITVECTOR_ROTATE_RIGHT_OP,
+ "rotate_right");
+ addIndexedOperator(
+ kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv");
+}
- Parser::addOperator(kind::BITVECTOR_BITOF);
- Parser::addOperator(kind::BITVECTOR_EXTRACT);
- Parser::addOperator(kind::BITVECTOR_REPEAT);
- Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND);
- Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND);
- Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT);
- Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT);
+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(kind::INT_TO_BITVECTOR);
- Parser::addOperator(kind::BITVECTOR_TO_NAT);
+ if (!strictModeEnabled())
+ {
+ addOperator(kind::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_CHARAT, "str.at" );
addOperator(kind::STRING_STRIDOF, "str.indexof" );
addOperator(kind::STRING_STRREPL, "str.replace" );
+ addOperator(kind::STRING_STRREPLALL, "str.replaceall");
+ if (!strictModeEnabled())
+ {
+ addOperator(kind::STRING_TOLOWER, "str.tolower");
+ addOperator(kind::STRING_TOUPPER, "str.toupper");
+ }
addOperator(kind::STRING_PREFIX, "str.prefixof" );
addOperator(kind::STRING_SUFFIX, "str.suffixof" );
- 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");
+ // at the moment, we only use this syntax for smt2.6.1
+ if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+ {
+ 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");
+ }
+ 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::REGEXP_CONCAT, "re.++");
addOperator(kind::REGEXP_UNION, "re.union");
addOperator(kind::REGEXP_INTER, "re.inter");
addOperator(kind::REGEXP_OPT, "re.opt");
addOperator(kind::REGEXP_RANGE, "re.range");
addOperator(kind::REGEXP_LOOP, "re.loop");
+ addOperator(kind::STRING_CODE, "str.code");
+ addOperator(kind::STRING_LT, "str.<");
+ addOperator(kind::STRING_LEQ, "str.<=");
}
void Smt2::addFloatingPointOperators() {
addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
- Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
- Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
- Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
- Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
- Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
- Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
- Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
+ addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
+ api::FLOATINGPOINT_TO_FP_GENERIC_OP,
+ "to_fp");
+ addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+ api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
+ "to_fp_unsigned");
+ addIndexedOperator(
+ kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv");
+ addIndexedOperator(
+ kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv");
+
+ if (!strictModeEnabled())
+ {
+ addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+ api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
+ "to_fp_bv");
+ addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+ api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
+ "to_fp_fp");
+ addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
+ api::FLOATINGPOINT_TO_FP_REAL_OP,
+ "to_fp_real");
+ addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+ api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
+ "to_fp_signed");
+ }
}
void Smt2::addSepOperators() {
defineType("Bool", getExprManager()->booleanType());
defineVar("true", getExprManager()->mkConst(true));
defineVar("false", getExprManager()->mkConst(false));
- Parser::addOperator(kind::AND);
- Parser::addOperator(kind::DISTINCT);
- Parser::addOperator(kind::EQUAL);
- Parser::addOperator(kind::IMPLIES);
- Parser::addOperator(kind::ITE);
- Parser::addOperator(kind::NOT);
- Parser::addOperator(kind::OR);
- Parser::addOperator(kind::XOR);
+ 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");
break;
case THEORY_REALS_INTS:
defineType("Real", getExprManager()->realType());
- Parser::addOperator(kind::DIVISION);
+ addOperator(kind::DIVISION, "/");
addOperator(kind::TO_INTEGER, "to_int");
addOperator(kind::IS_INTEGER, "is_int");
addOperator(kind::TO_REAL, "to_real");
addOperator(kind::INTS_DIVISION, "div");
addOperator(kind::INTS_MODULUS, "mod");
addOperator(kind::ABS, "abs");
- Parser::addOperator(kind::DIVISIBLE);
+ addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible");
break;
case THEORY_REALS:
defineType("Real", getExprManager()->realType());
addArithmeticOperators();
- Parser::addOperator(kind::DIVISION);
+ addOperator(kind::DIVISION, "/");
+ if (!strictModeEnabled())
+ {
+ addOperator(kind::ABS, "abs");
+ }
break;
- case THEORY_QUANTIFIERS:
+ case THEORY_TRANSCENDENTALS:
+ defineVar("real.pi",
+ getExprManager()->mkNullaryOperator(getExprManager()->realType(),
+ CVC4::kind::PI));
+ addTranscendentalOperators();
break;
+ case THEORY_QUANTIFIERS: addQuantifiersOperators(); break;
+
case THEORY_SETS:
+ defineVar("emptyset",
+ d_solver->mkEmptySet(d_solver->getNullSort()).getExpr());
+ // 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::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");
break;
case THEORY_DATATYPES:
- Parser::addOperator(kind::APPLY_CONSTRUCTOR);
- Parser::addOperator(kind::APPLY_TESTER);
- Parser::addOperator(kind::APPLY_SELECTOR);
- Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
+ {
+ const std::vector<Type> types;
+ defineType("Tuple", getExprManager()->mkTupleType(types));
+ addDatatypesOperators();
break;
+ }
case THEORY_STRINGS:
defineType("String", getExprManager()->stringType());
+ defineType("RegLan", getExprManager()->regExpType());
defineType("Int", getExprManager()->integerType());
+
+ defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
+ defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr());
+
addStringOperators();
break;
case THEORY_UF:
Parser::addOperator(kind::APPLY_UF);
+
+ if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
+ {
+ addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card");
+ addOperator(kind::CARDINALITY_VALUE, "fmf.card.val");
+ }
break;
case THEORY_FP:
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());
+ defineVar("roundTowardPositive",
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
+ defineVar("RTN",
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
+ defineVar("roundTowardNegative",
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
+ defineVar("RTZ",
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
+ defineVar("roundTowardZero",
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
+
addFloatingPointOperators();
break;
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());
+
addSepOperators();
break;
operatorKindMap[name] = kind;
}
+void Smt2::addIndexedOperator(Kind tKind,
+ api::Kind opKind,
+ const std::string& name)
+{
+ Parser::addOperator(tKind);
+ d_indexedOpKindMap[name] = opKind;
+}
+
Kind Smt2::getOperatorKind(const std::string& name) const {
// precondition: isOperatorEnabled(name)
return operatorKindMap.find(name)->second;
bool Smt2::isTheoryEnabled(Theory theory) const {
switch(theory) {
case THEORY_ARRAYS:
- return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
+ return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
case THEORY_BITVECTORS:
return d_logic.isTheoryEnabled(theory::THEORY_BV);
case THEORY_CORE:
}
Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
- if(sygus() && name[0]=='-' &&
- name.find_first_not_of("0123456789", 1) == std::string::npos) {
- //allow unary minus in sygus
+ if (sygus_v1() && name[0] == '-'
+ && name.find_first_not_of("0123456789", 1) == std::string::npos)
+ {
+ // allow unary minus in sygus version 1
return getExprManager()->mkConst(Rational(name));
- }else if(isAbstractValue(name)) {
+ }
+ else if (isAbstractValue(name))
+ {
return mkAbstractValue(name);
- }else{
- return Parser::getExpressionForNameAndType(name, t);
}
+ return Parser::getExpressionForNameAndType(name, t);
+}
+
+api::Term Smt2::mkIndexedConstant(const std::string& name,
+ const std::vector<uint64_t>& numerals)
+{
+ if (isTheoryEnabled(THEORY_FP))
+ {
+ if (name == "+oo")
+ {
+ return d_solver->mkPosInf(numerals[0], numerals[1]);
+ }
+ else if (name == "-oo")
+ {
+ return d_solver->mkNegInf(numerals[0], numerals[1]);
+ }
+ else if (name == "NaN")
+ {
+ return d_solver->mkNaN(numerals[0], numerals[1]);
+ }
+ else if (name == "+zero")
+ {
+ return d_solver->mkPosZero(numerals[0], numerals[1]);
+ }
+ else if (name == "-zero")
+ {
+ return d_solver->mkNegZero(numerals[0], numerals[1]);
+ }
+ }
+
+ if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0)
+ {
+ std::string bvStr = name.substr(2);
+ return d_solver->mkBitVector(numerals[0], bvStr, 10);
+ }
+
+ // NOTE: Theory parametric constants go here
+
+ parseError(std::string("Unknown indexed literal `") + name + "'");
+ return api::Term();
+}
+
+api::OpTerm Smt2::mkIndexedOp(const std::string& name,
+ const std::vector<uint64_t>& numerals)
+{
+ const auto& kIt = d_indexedOpKindMap.find(name);
+ if (kIt != d_indexedOpKindMap.end())
+ {
+ api::Kind k = (*kIt).second;
+ if (numerals.size() == 1)
+ {
+ return d_solver->mkOpTerm(k, numerals[0]);
+ }
+ else if (numerals.size() == 2)
+ {
+ return d_solver->mkOpTerm(k, numerals[0], numerals[1]);
+ }
+ }
+
+ parseError(std::string("Unknown indexed function `") + name + "'");
+ return api::OpTerm();
+}
+
+Expr Smt2::mkDefineFunRec(
+ const std::string& fname,
+ const std::vector<std::pair<std::string, Type> >& sortedVarNames,
+ Type t,
+ std::vector<Expr>& flattenVars)
+{
+ std::vector<Type> sorts;
+ for (const std::pair<std::string, CVC4::Type>& 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);
+
+ // allow overloading
+ return mkVar(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,
+ 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)
+ {
+ Expr v = mkBoundVar(svn.first, svn.second);
+ bvs.push_back(v);
+ }
+
+ bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
}
void Smt2::reset() {
}
void Smt2::resetAssertions() {
- this->Parser::reset();
+ // Remove all declarations except the ones at level 0.
+ while (this->scopeLevel() > 0) {
+ this->popScope();
+ }
}
-void Smt2::setLogic(std::string name) {
+Command* Smt2::setLogic(std::string name, bool fromCommand)
+{
+ if (fromCommand)
+ {
+ if (d_seenSetLogic)
+ {
+ parseError("Only one set-logic is allowed.");
+ }
+ d_seenSetLogic = true;
- if(sygus()) {
+ if (logicIsForced())
+ {
+ // If the logic is forced, we ignore all set-logic requests from commands.
+ return new EmptyCommand();
+ }
+ }
+
+ if (sygus_v1())
+ {
// non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
if(name == "Arrays") {
name = "A";
}
d_logicSet = true;
- if(logicIsForced()) {
- d_logic = getForcedLogic();
- } else {
- d_logic = name;
- }
-
- // if sygus is enabled, we must enable UF, datatypes and integer arithmetic
+ d_logic = name;
+
+ // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
+ // higher-order
if(sygus()) {
+ if (!d_logic.isQuantified())
+ {
+ warning("Logics in sygus are assumed to contain quantifiers.");
+ warning("Omit QF_ from the logic to avoid this warning.");
+ }
// get unlocked copy, modify, copy and relock
LogicInfo log(d_logic.getUnlockedCopy());
- log.enableTheory(theory::THEORY_UF);
- log.enableTheory(theory::THEORY_DATATYPES);
- log.enableIntegers();
+ // enable everything needed for sygus
+ log.enableSygus();
d_logic = log;
d_logic.lock();
}
} else if(d_logic.areRealsUsed()) {
addTheory(THEORY_REALS);
}
+
+ if (d_logic.areTranscendentalsUsed())
+ {
+ addTheory(THEORY_TRANSCENDENTALS);
+ }
}
- if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
+ if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
addTheory(THEORY_ARRAYS);
}
if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
addTheory(THEORY_SEP);
}
-
-}/* Smt2::setLogic() */
+
+ if (sygus())
+ {
+ return new SetBenchmarkLogicCommand(d_logic.getLogicString());
+ }
+ else
+ {
+ return new SetBenchmarkLogicCommand(name);
+ }
+} /* Smt2::setLogic() */
+
+bool Smt2::sygus() const
+{
+ InputLanguage ilang = getLanguage();
+ return ilang == language::input::LANG_SYGUS
+ || ilang == language::input::LANG_SYGUS_V2;
+}
+bool Smt2::sygus_v1() const
+{
+ return getLanguage() == language::input::LANG_SYGUS;
+}
void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
// TODO: ???
// TODO: ???
}
-void Smt2::checkThatLogicIsSet() {
- if( ! logicIsSet() ) {
- if(strictModeEnabled()) {
+void Smt2::checkThatLogicIsSet()
+{
+ if (!logicIsSet())
+ {
+ if (strictModeEnabled())
+ {
parseError("set-logic must appear before this point.");
- } else {
- warning("No set-logic command was given before this point.");
- warning("CVC4 will make all theories available.");
- warning("Consider setting a stricter logic for (likely) better performance.");
- warning("To suppress this warning in the future use (set-logic ALL).");
-
- setLogic("ALL");
-
- Command* c = new SetBenchmarkLogicCommand("ALL");
- c->setMuted(true);
- preemptCommand(c);
+ }
+ else
+ {
+ Command* cmd = nullptr;
+ if (logicIsForced())
+ {
+ cmd = setLogic(getForcedLogic(), false);
+ }
+ else
+ {
+ warning("No set-logic command was given before this point.");
+ warning("CVC4 will make all theories available.");
+ warning(
+ "Consider setting a stricter logic for (likely) better "
+ "performance.");
+ warning("To suppress this warning in the future use (set-logic ALL).");
+
+ cmd = setLogic("ALL", false);
+ }
+ preemptCommand(cmd);
}
}
}
}
}
-Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) {
- Expr e = mkBoundVar(name, type);
- d_sygusVars.push_back(e);
- d_sygusVarPrimed[e] = false;
- if( isPrimed ){
- std::stringstream ss;
- ss << name << "'";
- Expr ep = mkBoundVar(ss.str(), type);
- d_sygusVars.push_back(ep);
- d_sygusVarPrimed[ep] = true;
- }
- return e;
-}
-
void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
if( type.isInteger() ){
ops.push_back(getExprManager()->mkConst(Rational(0)));
std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
CVC4::Type& ret, bool isNested ){
if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){
- Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl;
+ Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
+ << ", isLet = "
+ << (sgt.d_gterm_type == SygusGTerm::gterm_let)
+ << std::endl;
Kind oldKind;
Kind newKind = kind::UNDEFINED_KIND;
//convert to UMINUS if one child of MINUS
oldKind = kind::MINUS;
newKind = kind::UMINUS;
}
- /*
- //convert to IFF if boolean EQUAL
- if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){
- Type ctn = sgt.d_children[0].d_type;
- std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn );
- if( it != sygus_to_builtin.end() && it->second.isBoolean() ){
- oldKind = kind::EQUAL;
- newKind = kind::IFF;
- }
- }
- */
if( newKind!=kind::UNDEFINED_KIND ){
Expr newExpr = getExprManager()->operatorOf(newKind);
Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
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;
- sygus_to_builtin_expr[t] = sop;
- //store that term sop has dedicated sygus type t
- if( d_sygus_bound_var_type.find( sop )==d_sygus_bound_var_type.end() ){
- d_sygus_bound_var_type[sop] = t;
+ // only cache if it is a singleton datatype (has unique expr)
+ if (ops[sub_dt_index].size() == 1)
+ {
+ sygus_to_builtin_expr[t] = sop;
+ // store that term sop has dedicated sygus type t
+ if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end())
+ {
+ d_sygus_bound_var_type[sop] = t;
+ }
}
}else{
std::vector< Expr > children;
children.push_back( it->second );
}
}
- Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop);
+ Kind sk = sop.getKind() != kind::BUILTIN
+ ? getKindForFunction(sop)
+ : getExprManager()->operatorToKind(sop);
Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
Expr e = getExprManager()->mkExpr( sk, children );
Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
cargs[index][dindex].pop_back();
collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
- Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl;
+ Debug("parser-sygus") << "Make define-fun with "
+ << cargs[index][dindex].size()
+ << " operator arguments and " << let_define_args.size()
+ << " provided arguments..." << std::endl;
+ if (cargs[index][dindex].size() != let_define_args.size())
+ {
+ std::stringstream ss;
+ ss << "Wrong number of let body terms." << std::endl;
+ parseError(ss.str());
+ }
std::vector<CVC4::Type> fsorts;
for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
Debug("parser-sygus") << " " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
Debug("parser-sygus") << " add constructors..." << std::endl;
- std::vector<std::string> df_name;
- std::vector<CVC4::Expr> df_op;
- std::vector< std::vector<Expr> > df_let_args;
- std::vector< Expr > df_let_body;
- //dt.mkSygusConstructors( ops, cnames, cargs, sygus_to_builtin,
- // d_sygus_let_func_to_vars, d_sygus_let_func_to_body, d_sygus_let_func_to_num_input_vars,
- // df_name, df_op, df_let_args, df_let_body );
Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
Debug("parser-sygus") << " add constructors..." << std::endl;
- for( int i=0; i<(int)cnames.size(); i++ ){
+ // size of cnames changes, this loop must check size
+ for (unsigned i = 0; i < cnames.size(); i++)
+ {
bool is_dup = false;
bool is_dup_op = false;
- Expr let_body;
- std::vector< Expr > let_args;
- unsigned let_num_input_args = 0;
- for( int j=0; j<i; j++ ){
+ for (unsigned j = 0; j < i; j++)
+ {
if( ops[i]==ops[j] ){
is_dup_op = true;
if( cargs[i].size()==cargs[j].size() ){
}
}
}
+ Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
if( is_dup ){
- Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << " at " << i << std::endl;
+ Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
ops.erase( ops.begin() + i, ops.begin() + i + 1 );
cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
i--;
- }else if( is_dup_op ){
- Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << " at " << i << std::endl;
- //make into define-fun
- std::vector<CVC4::Type> fsorts;
- for( unsigned j=0; j<cargs[i].size(); j++ ){
- Type bt = sygus_to_builtin[cargs[i][j]];
- std::stringstream ss;
- ss << dt.getName() << "_x_" << i << "_" << j;
- Expr v = mkBoundVar(ss.str(), bt);
- let_args.push_back( v );
- fsorts.push_back( bt );
- Debug("parser-sygus") << ": var " << i << " " << v << " with type " << bt << " from " << cargs[i][j] << std::endl;
+ }
+ else
+ {
+ std::shared_ptr<SygusPrintCallback> spc;
+ if (is_dup_op)
+ {
+ Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
+ << std::endl;
+ // make into define-fun
+ std::vector<Type> 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);
+
+ // make the let_body
+ std::vector<Expr> children;
+ if (ops[i].getKind() != kind::BUILTIN)
+ {
+ children.push_back(ops[i]);
+ }
+ children.insert(children.end(), largs.begin(), largs.end());
+ Kind sk = ops[i].getKind() != kind::BUILTIN
+ ? kind::APPLY_UF
+ : getExprManager()->operatorToKind(ops[i]);
+ Expr body = getExprManager()->mkExpr(sk, children);
+ // replace by lambda
+ ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+ Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl;
+ // callback prints as the expression
+ spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
}
- //make the let_body
- std::vector< Expr > children;
- if( ops[i].getKind() != kind::BUILTIN ){
- children.push_back( ops[i] );
+ else
+ {
+ std::map<Expr, Expr>::iterator it =
+ d_sygus_let_func_to_body.find(ops[i]);
+ if (it != d_sygus_let_func_to_body.end())
+ {
+ Debug("parser-sygus") << "--> Let expression " << ops[i] << std::endl;
+ Expr let_body = it->second;
+ std::vector<Expr> let_args = d_sygus_let_func_to_vars[ops[i]];
+ unsigned let_num_input_args =
+ d_sygus_let_func_to_num_input_vars[ops[i]];
+ // the operator is just the body for the arguments
+ std::vector<Type> ltypes;
+ for (unsigned j = 0, size = let_args.size(); j < size; j++)
+ {
+ ltypes.push_back(let_args[j].getType());
+ }
+ std::vector<Expr> largs;
+ Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
+ Expr sbody = let_body.substitute(let_args, largs);
+ ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, sbody);
+ Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl;
+ // callback prints as a let expression
+ spc = std::make_shared<printer::SygusLetExprPrintCallback>(
+ let_body, let_args, let_num_input_args);
+ }
+ else if (ops[i].getType().isBitVector() && ops[i].isConst())
+ {
+ Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " ("
+ << cnames[i] << ")" << std::endl;
+ // Since there are multiple output formats for bit-vectors and
+ // we are required by sygus standards to print in the exact input
+ // format given by the user, we use a print callback to custom print
+ // the given name.
+ spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
+ }
+ else if (isDefinedFunction(ops[i]))
+ {
+ 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 (ops[i].getType().isFunction())
+ {
+ std::vector<Type> ftypes =
+ static_cast<FunctionType>(ops[i].getType()).getArgTypes();
+ std::vector<Expr> largs;
+ Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
+ largs.insert(largs.begin(), ops[i]);
+ Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
+ ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+ Debug("parser-sygus") << " ...replace op : " << ops[i]
+ << std::endl;
+ }
+ else
+ {
+ Debug("parser-sygus") << " ...replace op : " << ops[i]
+ << std::endl;
+ }
+ // keep a callback to say it should be printed with the defined name
+ spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
+ }
+ else
+ {
+ Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
+ }
}
- children.insert( children.end(), let_args.begin(), let_args.end() );
- Kind sk = ops[i].getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(ops[i]);
- Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl;
- let_body = getExprManager()->mkExpr( sk, children );
- Debug("parser-sygus") << ": new body of function is " << let_body << std::endl;
-
- Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
- Debug("parser-sygus") << ": function type is " << ft << std::endl;
+ // must rename to avoid duplication
std::stringstream ss;
- ss << dt.getName() << "_df_" << i;
- //replace operator and name
- ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+ ss << dt.getName() << "_" << i << "_" << cnames[i];
cnames[i] = ss.str();
- // indicate we need a define function
- df_name.push_back( ss.str() );
- df_op.push_back( ops[i] );
- df_let_args.push_back( let_args );
- df_let_body.push_back( let_body );
-
- //d_sygus_defined_funs.push_back( ops[i] );
- //preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
- dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, 0 );
- }else{
- std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] );
- if( it!=d_sygus_let_func_to_body.end() ){
- let_body = it->second;
- let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() );
- let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]];
- }
- dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args );
+ Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..."
+ << std::endl;
+ // add the sygus constructor
+ dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc);
+ Debug("parser-sygus") << " finished constructing the datatype"
+ << std::endl;
}
}
//identity element
Type bt = dt.getSygusType();
Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl;
+
std::stringstream ss;
- ss << t << "_x_id";
- Expr let_body = mkBoundVar(ss.str(), bt);
- std::vector< Expr > let_args;
- let_args.push_back( let_body );
- //make the identity function
- Type ft = getExprManager()->mkFunctionType(bt, bt);
- std::stringstream ssid;
- ssid << unresolved_gterm_sym[i] << "_id";
- Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
- // indicate we need a define function
- df_name.push_back( ssid.str() );
- df_op.push_back( id_op );
- df_let_args.push_back( let_args );
- df_let_body.push_back( let_body );
-
- //d_sygus_defined_funs.push_back( id_op );
- //preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
+ ss << t << "_x";
+ Expr var = mkBoundVar(ss.str(), bt);
+ std::vector<Expr> lchildren;
+ lchildren.push_back(
+ getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
+ lchildren.push_back(var);
+ Expr id_op = getExprManager()->mkExpr(kind::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;
id_carg.push_back( t );
- dt.addSygusConstructor( id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 );
+ dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
+
//add to operators
ops.push_back( id_op );
}
}
}
}
-
-
- for( unsigned i=0; i<df_name.size(); i++ ){
- d_sygus_defined_funs.push_back( df_op[i] );
- preemptCommand( new DefineFunctionCommand(df_name[i], df_op[i], df_let_args[i], df_let_body[i]) );
+}
+
+Expr Smt2::makeSygusBoundVarList(Datatype& dt,
+ unsigned i,
+ const std::vector<Type>& ltypes,
+ std::vector<Expr>& 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]);
+ lvars.push_back(v);
}
+ return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
}
-const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
- for( unsigned i=0; i<d_sygusVars.size(); i++ ){
- Expr v = d_sygusVars[i];
- std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
- if( it!=d_sygusVarPrimed.end() ){
- if( it->second==isPrimed ){
- vars.push_back( v );
+void Smt2::addSygusConstructorTerm(Datatype& dt,
+ Expr term,
+ std::map<Expr, Type>& ntsToUnres) const
+{
+ Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
+ // 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.
+ // Notice that let expressions are forbidden in the input syntax of term, so
+ // this does not lead to exponential behavior with respect to input size.
+ std::vector<Expr> args;
+ std::vector<Type> cargs;
+ Expr op = purifySygusGTerm(term, ntsToUnres, args, cargs);
+ Trace("parser-sygus2") << "Purified operator " << op
+ << ", #args/cargs=" << args.size() << "/"
+ << cargs.size() << std::endl;
+ std::shared_ptr<SygusPrintCallback> spc;
+ // callback prints as the expression
+ spc = std::make_shared<printer::SygusExprPrintCallback>(op, args);
+ if (!args.empty())
+ {
+ bool pureVar = false;
+ if (op.getNumChildren() == args.size())
+ {
+ pureVar = true;
+ for (unsigned i = 0, nchild = op.getNumChildren(); i < nchild; i++)
+ {
+ if (op[i] != args[i])
+ {
+ pureVar = false;
+ break;
+ }
}
- }else{
- //should never happen
+ }
+ Trace("parser-sygus2") << "Pure var is " << pureVar
+ << ", hasOp=" << op.hasOperator() << std::endl;
+ if (pureVar && op.hasOperator())
+ {
+ // optimization: use just the operator if it an application to only vars
+ op = op.getOperator();
+ }
+ else
+ {
+ Expr lbvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, args);
+ // its operator is a lambda
+ op = getExprManager()->mkExpr(kind::LAMBDA, lbvl, op);
+ }
+ }
+ Trace("parser-sygus2") << "Generated operator " << op << std::endl;
+ std::stringstream ss;
+ ss << op.getKind();
+ dt.addSygusConstructor(op, ss.str(), cargs, spc);
+}
+
+Expr Smt2::purifySygusGTerm(Expr term,
+ std::map<Expr, Type>& ntsToUnres,
+ std::vector<Expr>& args,
+ std::vector<Type>& cargs) const
+{
+ Trace("parser-sygus2-debug")
+ << "purifySygusGTerm: " << term << " #nchild=" << term.getNumChildren()
+ << std::endl;
+ std::map<Expr, Type>::iterator itn = ntsToUnres.find(term);
+ if (itn != ntsToUnres.end())
+ {
+ Expr ret = getExprManager()->mkBoundVar(term.getType());
+ Trace("parser-sygus2-debug")
+ << "...unresolved non-terminal, intro " << ret << std::endl;
+ args.push_back(ret);
+ cargs.push_back(itn->second);
+ return ret;
+ }
+ std::vector<Expr> pchildren;
+ // To test whether the operator should be passed to mkExpr below, we check
+ // whether this term has an operator which is not constant. This includes
+ // APPLY_UF terms, but excludes applications of interpreted symbols.
+ if (term.hasOperator() && !term.getOperator().isConst())
+ {
+ pchildren.push_back(term.getOperator());
+ }
+ bool childChanged = false;
+ for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++)
+ {
+ Trace("parser-sygus2-debug")
+ << "......purify child " << i << " : " << term[i] << std::endl;
+ Expr ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
+ pchildren.push_back(ptermc);
+ childChanged = childChanged || ptermc != term[i];
+ }
+ if (!childChanged)
+ {
+ Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
+ return term;
+ }
+ Expr nret = getExprManager()->mkExpr(term.getKind(), pchildren);
+ Trace("parser-sygus2-debug")
+ << "...child changed, return " << nret << std::endl;
+ return nret;
+}
+
+void Smt2::addSygusConstructorVariables(Datatype& dt,
+ std::vector<Expr>& sygusVars,
+ Type 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)
+ {
+ std::stringstream ss;
+ ss << v;
+ std::vector<CVC4::Type> cargs;
+ dt.addSygusConstructor(v, ss.str(), cargs);
}
}
}
-const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
- // When constructing the synthesis conjecture, we quantify on the
- // (higher-order) bound variable synth_fun.
- d_sygusFunSymbols.push_back(synth_fun);
-
- // Variable "sfproxy" carries the type, which may be a SyGuS datatype
- // that corresponds to syntactic restrictions.
- Expr sym = mkBoundVar("sfproxy", t);
- std::vector< Expr > attr_value;
- attr_value.push_back(sym);
- Command* cattr =
- new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value);
- cattr->setMuted(true);
- preemptCommand(cattr);
+InputLanguage Smt2::getLanguage() const
+{
+ ExprManager* em = getExprManager();
+ return em->getOptions().getInputLanguage();
}
-}/* CVC4::parser namespace */
+} // namespace parser
}/* CVC4 namespace */
projects / cvc5.git / blobdiff