** Top contributors (to current version):
** Andrew Reynolds, Kshitij Bansal, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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>
+
// ANTLR defines these, which is really bad!
#undef true
#undef false
namespace CVC4 {
namespace parser {
-Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
- Parser(exprManager,input,strictMode,parseOnly),
- d_logicSet(false),
- d_nextSygusFun(0) {
- d_unsatCoreNames.push(std::map<Expr, std::string>());
- 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::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_U16TOS, "u16.to.str" );
- addOperator(kind::STRING_STOU16, "str.to.u16" );
- addOperator(kind::STRING_U32TOS, "u32.to.str" );
- addOperator(kind::STRING_STOU32, "str.to.u32" );
- 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::IFF);
- 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::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");
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:
return d_logicSet;
}
+Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
+ 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))
+ {
+ return mkAbstractValue(name);
+ }
+ 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() {
d_logicSet = false;
d_logic = LogicInfo();
operatorKindMap.clear();
d_lastNamedTerm = std::pair<Expr, std::string>();
- d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
this->Parser::reset();
- d_unsatCoreNames.push(std::map<Expr, std::string>());
if( !strictModeEnabled() ) {
addTheory(Smt2::THEORY_CORE);
}
}
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) {
- if(sygus()) {
+Command* Smt2::setLogic(std::string name, bool fromCommand)
+{
+ if (fromCommand)
+ {
+ if (d_seenSetLogic)
+ {
+ parseError("Only one set-logic is allowed.");
+ }
+ d_seenSetLogic = true;
+
+ 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 = "AUF";
- } else if(name == "Reals") {
- name = "UFLRA";
- } else if(name == "LIA") {
- name = "UFLIA";
- } else if(name == "LRA") {
- name = "UFLRA";
- } else if(name == "LIRA") {
- name = "UFLIRA";
- } else if(name == "BV") {
- name = "UFBV";
- } else if(name == "SLIA") {
- name = "UFSLIA";
- } else if(name == "SAT") {
- name = "UF";
- } else if(name == "ALL" || name == "ALL_SUPPORTED") {
- //no change
- } else {
- std::stringstream ss;
- ss << "Unknown SyGuS background logic `" << name << "'";
- parseError(ss.str());
+ name = "A";
+ }else if(name == "Reals") {
+ name = "LRA";
}
}
d_logicSet = true;
- if(logicIsForced()) {
- d_logic = getForcedLogic();
- } else {
- d_logic = name;
+ 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());
+ // enable everything needed for sygus
+ log.enableSygus();
+ d_logic = log;
+ d_logic.lock();
}
// Core theory belongs to every logic
} 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 {
- if(sygus()) {
- setLogic("LIA");
- } else {
+ }
+ 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(
+ "Consider setting a stricter logic for (likely) better "
+ "performance.");
warning("To suppress this warning in the future use (set-logic ALL).");
- setLogic("ALL");
+ cmd = setLogic("ALL", false);
}
-
- Command* c = new SetBenchmarkLogicCommand("ALL");
- c->setMuted(true);
- preemptCommand(c);
+ 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 collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::map< Type, std::vector< DatatypeConstructorArg > >& sels ){
- if( !range.isBoolean() ){
- if( std::find( types.begin(), types.end(), range )==types.end() ){
- Debug("parser-sygus") << "...will make grammar for " << range << std::endl;
- types.push_back( range );
- if( range.isDatatype() ){
- const Datatype& dt = ((DatatypeType)range).getDatatype();
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- Type crange = ((SelectorType)dt[i][j].getType()).getRangeType();
- sels[crange].push_back( dt[i][j] );
- collectSygusGrammarTypesFor( crange, types, sels );
- }
- }
- }
- }
- }
-}
-
-void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
- std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) {
-
- //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
- // parseError("No default grammar for type.");
- //}
- startIndex = -1;
- Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
- std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
-
- std::vector< Type > types;
- std::map< Type, std::vector< DatatypeConstructorArg > > sels;
- //types for each of the variables
- for( unsigned i=0; i<sygus_vars.size(); i++ ){
- collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
- }
- //types connected to range
- collectSygusGrammarTypesFor( range, types, sels );
-
- //name of boolean sort
- std::stringstream ssb;
- ssb << fun << "_Bool";
- std::string dbname = ssb.str();
- Type unres_bt = mkUnresolvedType(ssb.str());
-
- std::vector< Type > unres_types;
- std::map< Type, Type > type_to_unres;
- for( unsigned i=0; i<types.size(); i++ ){
- std::stringstream ss;
- ss << fun << "_" << types[i];
- std::string dname = ss.str();
- datatypes.push_back(Datatype(dname));
- ops.push_back(std::vector<Expr>());
- //make unresolved type
- Type unres_t = mkUnresolvedType(dname);
- unres_types.push_back(unres_t);
- type_to_unres[types[i]] = unres_t;
- sygus_to_builtin[unres_t] = types[i];
- }
- for( unsigned i=0; i<types.size(); i++ ){
- Debug("parser-sygus") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
- std::vector<std::string> cnames;
- std::vector<std::vector<CVC4::Type> > cargs;
- std::vector<std::string> unresolved_gterm_sym;
- Type unres_t = unres_types[i];
- //add variables
- for( unsigned j=0; j<sygus_vars.size(); j++ ){
- if( sygus_vars[j].getType()==types[i] ){
- std::stringstream ss;
- ss << sygus_vars[j];
- Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
- ops[i].push_back( sygus_vars[j] );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- }
- }
- //add constants
- std::vector< Expr > consts;
- mkSygusConstantsForType( types[i], consts );
- for( unsigned j=0; j<consts.size(); j++ ){
- std::stringstream ss;
- ss << consts[j];
- Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
- ops[i].push_back( consts[j] );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- }
- //ITE
- CVC4::Kind k = kind::ITE;
- Debug("parser-sygus") << "...add for " << k << std::endl;
- ops[i].push_back(getExprManager()->operatorOf(k));
- cnames.push_back( kind::kindToString(k) );
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_bt);
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_t);
-
- if( types[i].isInteger() ){
- for( unsigned j=0; j<2; j++ ){
- CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS;
- Debug("parser-sygus") << "...add for " << k << std::endl;
- ops[i].push_back(getExprManager()->operatorOf(k));
- cnames.push_back(kind::kindToString(k));
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_t);
- }
- }else if( types[i].isDatatype() ){
- Debug("parser-sygus") << "...add for constructors" << std::endl;
- const Datatype& dt = ((DatatypeType)types[i]).getDatatype();
- for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
- Debug("parser-sygus") << "...for " << dt[k].getName() << std::endl;
- ops[i].push_back( dt[k].getConstructor() );
- cnames.push_back( dt[k].getName() );
- cargs.push_back( std::vector< CVC4::Type >() );
- for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){
- Type crange = ((SelectorType)dt[k][j].getType()).getRangeType();
- //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
- cargs.back().push_back( type_to_unres[crange] );
- }
- }
- }else{
- std::stringstream sserr;
- sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
- warning(sserr.str());
- }
- //add for all selectors to this type
- if( !sels[types[i]].empty() ){
- Debug("parser-sygus") << "...add for selectors" << std::endl;
- for( unsigned j=0; j<sels[types[i]].size(); j++ ){
- Debug("parser-sygus") << "...for " << sels[types[i]][j].getName() << std::endl;
- Type arg_type = ((SelectorType)sels[types[i]][j].getType()).getDomain();
- ops[i].push_back( sels[types[i]][j].getSelector() );
- cnames.push_back( sels[types[i]][j].getName() );
- cargs.push_back( std::vector< CVC4::Type >() );
- //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() );
- cargs.back().push_back( type_to_unres[arg_type] );
- }
- }
- Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
- datatypes[i].setSygus( types[i], bvl, true, true );
- mkSygusDatatype( datatypes[i], ops[i], cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
- sorts.push_back( types[i] );
- //set start index if applicable
- if( types[i]==range ){
- startIndex = i;
- }
- }
-
- //make Boolean type
- Type btype = getExprManager()->booleanType();
- datatypes.push_back(Datatype(dbname));
- ops.push_back(std::vector<Expr>());
- std::vector<std::string> cnames;
- std::vector<std::vector<CVC4::Type> > cargs;
- std::vector<std::string> unresolved_gterm_sym;
- Debug("parser-sygus") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
- //add variables
- for( unsigned i=0; i<sygus_vars.size(); i++ ){
- if( sygus_vars[i].getType().isBoolean() ){
- std::stringstream ss;
- ss << sygus_vars[i];
- Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
- ops.back().push_back( sygus_vars[i] );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- }
- }
- //add constants if no variables and no connected types
- if( ops.back().empty() && types.empty() ){
- std::vector< Expr > consts;
- mkSygusConstantsForType( btype, consts );
- for( unsigned j=0; j<consts.size(); j++ ){
- std::stringstream ss;
- ss << consts[j];
- Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
- ops.back().push_back( consts[j] );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- }
- }
- //add operators
- for( unsigned i=0; i<3; i++ ){
- CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR );
- Debug("parser-sygus") << "...add for " << k << std::endl;
- ops.back().push_back(getExprManager()->operatorOf(k));
- cnames.push_back(kind::kindToString(k));
- cargs.push_back( std::vector< CVC4::Type >() );
- if( k==kind::NOT ){
- cargs.back().push_back(unres_bt);
- }else if( k==kind::AND || k==kind::OR ){
- cargs.back().push_back(unres_bt);
- cargs.back().push_back(unres_bt);
- }
- }
- //add predicates for types
- for( unsigned i=0; i<types.size(); i++ ){
- Debug("parser-sygus") << "...add predicates for " << types[i] << std::endl;
- //add equality per type
- CVC4::Kind k = kind::EQUAL;
- Debug("parser-sygus") << "...add for " << k << std::endl;
- ops.back().push_back(getExprManager()->operatorOf(k));
- std::stringstream ss;
- ss << kind::kindToString(k) << "_" << types[i];
- cnames.push_back(ss.str());
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- cargs.back().push_back(unres_types[i]);
- //type specific predicates
- if( types[i].isInteger() ){
- CVC4::Kind k = kind::LEQ;
- Debug("parser-sygus") << "...add for " << k << std::endl;
- ops.back().push_back(getExprManager()->operatorOf(k));
- cnames.push_back(kind::kindToString(k));
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- cargs.back().push_back(unres_types[i]);
- }else if( types[i].isDatatype() ){
- //add for testers
- Debug("parser-sygus") << "...add for testers" << std::endl;
- const Datatype& dt = ((DatatypeType)types[i]).getDatatype();
- for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
- Debug("parser-sygus") << "...for " << dt[k].getTesterName() << std::endl;
- ops.back().push_back(dt[k].getTester());
- cnames.push_back(dt[k].getTesterName());
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- }
- }
- }
- if( range==btype ){
- startIndex = sorts.size();
- }
- Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
- datatypes.back().setSygus( btype, bvl, true, true );
- mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
- sorts.push_back( btype );
-
- Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl;
-}
-
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;
}
}
-void Smt2::defineSygusFuns() {
- // only define each one once
- while(d_nextSygusFun < d_sygusFuns.size()) {
- std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
- std::string fun = p.first;
- Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl;
- Expr eval = p.second;
- FunctionType evalType = eval.getType();
- std::vector<Type> argTypes = evalType.getArgTypes();
- Type rangeType = evalType.getRangeType();
- Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl;
-
- // first make the function type
- std::vector<Expr> sygusVars;
- std::vector<Type> funType;
- for(size_t j = 1; j < argTypes.size(); ++j) {
- funType.push_back(argTypes[j]);
- std::stringstream ss;
- ss << fun << "_v_" << j;
- sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j]));
- }
- Type funt;
- if( !funType.empty() ){
- funt = getExprManager()->mkFunctionType(funType, rangeType);
- Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
-
- // copy the bound vars
- /*
- std::vector<Expr> sygusVars;
- //std::vector<Type> types;
- for(size_t i = 0; i < d_sygusVars.size(); ++i) {
- std::stringstream ss;
- ss << d_sygusVars[i];
- Type type = d_sygusVars[i].getType();
- sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
- //types.push_back(type);
- }
- Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
- */
-
- //Type t = getExprManager()->mkFunctionType(types, rangeType);
- //Debug("parser-sygus") << "...function type : " << t << std::endl;
- }else{
- funt = rangeType;
- }
- Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED);
- Debug("parser-sygus") << "...made function : " << lambda << std::endl;
- std::vector<Expr> applyv;
- Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]);
- d_sygusFunSymbols.push_back(funbv);
- applyv.push_back(eval);
- applyv.push_back(funbv);
- for(size_t i = 0; i < sygusVars.size(); ++i) {
- applyv.push_back(sygusVars[i]);
- }
- Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
- Debug("parser-sygus") << "...made apply " << apply << std::endl;
- Debug("parser-sygus") << "--> Define " << fun << " as " << lambda << " " << apply << std::endl;
- Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
- preemptCommand(cmd);
-
- ++d_nextSygusFun;
- }
-}
-
void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
std::vector<std::string>& unresolved_gterm_sym,
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;
- for( int i=0; i<(int)cnames.size(); i++ ){
+
+ Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
+ Debug("parser-sygus") << " add constructors..." << std::endl;
+ // 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();
- d_sygus_defined_funs.push_back( ops[i] );
- preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
- addSygusDatatypeConstructor( dt, 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]];
- }
- addSygusDatatypeConstructor( dt, 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;
}
}
+
Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl;
if( !unresolved_gterm_sym.empty() ){
std::vector< Type > types;
//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);
- 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 );
- addSygusDatatypeConstructor( dt, 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 );
}
}
}
}
-
}
-void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
- CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) {
- Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl;
- if( !let_body.isNull() ){
- Debug("parser-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl;
- //TODO : remove arguments not occurring in body
- //if this is a self identity function, ignore
- if( let_args.size()==0 && let_args[0]==let_body ){
- Debug("parser-sygus") << " identity function " << cargs[0] << " to " << dt.getName() << std::endl;
- //TODO
- }
- }
- std::string name = dt.getName() + "_" + cname;
- std::string testerId("is-");
- testerId.append(name);
- checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
- checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
- CVC4::DatatypeConstructor c(name, testerId );
- c.setSygus( op, let_body, let_args, let_num_input_args );
- for( unsigned j=0; j<cargs.size(); j++ ){
- Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl;
- std::stringstream sname;
- sname << name << "_" << j;
- c.addArg(sname.str(), cargs[j]);
+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);
}
- dt.addConstructor(c);
+ return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
}
-
-// i is index in datatypes/ops
-// j is index is datatype
-Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
- std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
- Expr eval, const Datatype& dt, size_t i, size_t j ) {
- const DatatypeConstructor& ctor = dt[j];
- Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
- std::vector<Expr> bvs, extraArgs;
- for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
- std::string vname = "v_" + ctor[k].getName();
- Expr bv = getExprManager()->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType());
- bvs.push_back(bv);
- extraArgs.push_back(bv);
- }
- if( !terms[0].isNull() ){
- bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
- }
- Expr bvl;
- if( !bvs.empty() ){
- bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs);
- }
- Debug("parser-sygus") << "...made bv list " << bvl << std::endl;
- std::vector<Expr> patv;
- patv.push_back(eval);
- std::vector<Expr> applyv;
- applyv.push_back(ctor.getConstructor());
- applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end());
- for(size_t k = 0; k < applyv.size(); ++k) {
- }
- Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
- Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl;
- patv.push_back(cpatv);
- if( !terms[0].isNull() ){
- patv.insert(patv.end(), terms[0].begin(), terms[0].end());
- }
- Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
- Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
- std::vector<Expr> builtApply;
- for(size_t k = 0; k < extraArgs.size(); ++k) {
- std::vector<Expr> patvb;
- patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]);
- patvb.push_back(extraArgs[k]);
- if( !terms[0].isNull() ){
- patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
- }
- Debug("parser-sygus-debug") << "...add to built apply " << evals[DatatypeType(extraArgs[k].getType())] << " " << extraArgs[k] << " " << extraArgs[k].getType() << std::endl;
- builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb));
- Debug("parser-sygus-debug") << "...added " << builtApply.back() << std::endl;
- }
- for(size_t k = 0; k < builtApply.size(); ++k) {
- }
- Expr builtTerm;
- Debug("parser-sygus") << "...operator is : " << ops[i][j] << ", type = " << ops[i][j].getType() << ", kind = " << ops[i][j].getKind() << ", is defined = " << isDefinedFunction( ops[i][j] ) << std::endl;
- if( ops[i][j].getKind() != kind::BUILTIN ){
- Kind ok = kind::UNDEFINED_KIND;
- if( isDefinedFunction( ops[i][j] ) || std::find( d_sygus_defined_funs.begin(), d_sygus_defined_funs.end(), ops[i][j] )!=d_sygus_defined_funs.end() ){
- ok = kind::APPLY;
- }else{
- Type t = ops[i][j].getType();
- if( t.isConstructor() ){
- ok = kind::APPLY_CONSTRUCTOR;
- }else if( t.isSelector() ){
- ok = kind::APPLY_SELECTOR;
- }else if( t.isTester() ){
- ok = kind::APPLY_TESTER;
- }else{
- ok = getExprManager()->operatorToKind( ops[i][j] );
+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;
+ }
}
}
- Debug("parser-sygus") << "...processed operator kind : " << ok << std::endl;
- if( ok!=kind::UNDEFINED_KIND ){
- builtTerm = getExprManager()->mkExpr(ok, ops[i][j], builtApply);
- }else{
- builtTerm = ops[i][j];
+ 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{
- if( !builtApply.empty() ){
- builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
- }else{
- builtTerm = ops[i][j];
+ else
+ {
+ Expr lbvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, args);
+ // its operator is a lambda
+ op = getExprManager()->mkExpr(kind::LAMBDA, lbvl, op);
}
}
- Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
- Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
- if( !bvl.isNull() ){
- Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
- pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
- assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
+ 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;
}
- Debug("parser-sygus") << "...made assertion " << assertion << std::endl;
-
- //linearize multiplication if possible
- if( builtTerm.getKind()==kind::MULT ){
- for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
- Type at = SelectorType(ctor[k].getType()).getRangeType();
- if( at.isDatatype() ){
- DatatypeType atd = (DatatypeType)SelectorType(ctor[k].getType()).getRangeType();
- Debug("parser-sygus") << "Argument " << k << " " << atd << std::endl;
- std::vector<DatatypeType>::iterator itd = std::find( datatypeTypes.begin(), datatypeTypes.end(), atd );
- if( itd!=datatypeTypes.end() ){
- Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl;
- unsigned index = itd-datatypeTypes.begin();
- Debug("parser-sygus2") << "index = " << index << std::endl;
- bool isConst = true;
- for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
- Debug("parser-sygus2") << "ops[" << cc << "]=" << ops[index][cc] << std::endl;
- if( ops[index][cc].getKind() != kind::CONST_RATIONAL ){
- isConst = false;
- break;
- }
- }
- if( isConst ){
- Debug("parser-sygus") << "Linearize multiplication " << ctor << " based on argument " << k << std::endl;
- const Datatype & atdd = atd.getDatatype();
- std::vector<Expr> assertions;
- std::vector<Expr> nbvs;
- for( unsigned a=0; a<bvl.getNumChildren(); a++ ){
- if( a!=k ){
- nbvs.push_back( bvl[a] );
- }
- }
- Expr nbvl = getExprManager()->mkExpr( kind::BOUND_VAR_LIST, nbvs );
- for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
- //Make new assertion based on partially instantiating existing
- applyv[k+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, atdd[cc].getConstructor());
- Debug("parser-sygus") << "applyv " << applyv[k+1] << std::endl;
- cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
- Debug("parser-sygus") << "cpatv " << cpatv << std::endl;
- patv[1] = cpatv;
- evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
- Debug("parser-sygus") << "evalApply " << evalApply << std::endl;
- builtApply[k] = ops[index][cc];
- Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
- builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
- Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
- Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
- Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
- epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
- eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
- assertions.push_back( eassertion );
- }
- assertion = assertions.size()==1 ? assertions[0] : getExprManager()->mkExpr( kind::AND, assertions );
- Debug("parser-sygus") << "...(linearized) assertion is: " << assertion << std::endl;
- }
- }
- }
- }
+ 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];
}
- return assertion;
+ 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;
}
-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 );
- }
- }else{
- //should never happen
+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);
}
}
}
-}/* CVC4::parser namespace */
+InputLanguage Smt2::getLanguage() const
+{
+ ExprManager* em = getExprManager();
+ return em->getOptions().getInputLanguage();
+}
+
+} // namespace parser
}/* CVC4 namespace */
projects / cvc5.git / blobdiff