/*! \file smt2.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Kshitij Bansal, Morgan Deters
+ ** Andrew Reynolds, Andres Noetzli, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 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 <algorithm>
+
+#include "base/check.h"
#include "options/options.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/smt2/smt2_input.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(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
- : Parser(solver, input, strictMode, parseOnly),
+Smt2::Smt2(api::Solver* solver,
+ SymbolManager* sm,
+ Input* input,
+ bool strictMode,
+ bool parseOnly)
+ : Parser(solver, sm, input, strictMode, parseOnly),
d_logicSet(false),
d_seenSetLogic(false)
{
- if (!strictModeEnabled())
- {
- addTheory(Smt2::THEORY_CORE);
- }
}
+Smt2::~Smt2() {}
+
void Smt2::addArithmeticOperators() {
- addOperator(kind::PLUS, "+");
- addOperator(kind::MINUS, "-");
- // kind::MINUS is converted to kind::UMINUS if there is only a single operand
- Parser::addOperator(kind::UMINUS);
- addOperator(kind::MULT, "*");
- addOperator(kind::LT, "<");
- addOperator(kind::LEQ, "<=");
- addOperator(kind::GT, ">");
- addOperator(kind::GEQ, ">=");
+ addOperator(api::PLUS, "+");
+ addOperator(api::MINUS, "-");
+ // api::MINUS is converted to api::UMINUS if there is only a single operand
+ Parser::addOperator(api::UMINUS);
+ addOperator(api::MULT, "*");
+ addOperator(api::LT, "<");
+ addOperator(api::LEQ, "<=");
+ addOperator(api::GT, ">");
+ addOperator(api::GEQ, ">=");
if (!strictModeEnabled())
{
// NOTE: this operator is non-standard
- addOperator(kind::POW, "^");
+ addOperator(api::POW, "^");
}
}
void Smt2::addTranscendentalOperators()
{
- addOperator(kind::EXPONENTIAL, "exp");
- addOperator(kind::SINE, "sin");
- addOperator(kind::COSINE, "cos");
- addOperator(kind::TANGENT, "tan");
- addOperator(kind::COSECANT, "csc");
- addOperator(kind::SECANT, "sec");
- addOperator(kind::COTANGENT, "cot");
- addOperator(kind::ARCSINE, "arcsin");
- addOperator(kind::ARCCOSINE, "arccos");
- addOperator(kind::ARCTANGENT, "arctan");
- addOperator(kind::ARCCOSECANT, "arccsc");
- addOperator(kind::ARCSECANT, "arcsec");
- addOperator(kind::ARCCOTANGENT, "arccot");
- addOperator(kind::SQRT, "sqrt");
+ addOperator(api::EXPONENTIAL, "exp");
+ addOperator(api::SINE, "sin");
+ addOperator(api::COSINE, "cos");
+ addOperator(api::TANGENT, "tan");
+ addOperator(api::COSECANT, "csc");
+ addOperator(api::SECANT, "sec");
+ addOperator(api::COTANGENT, "cot");
+ addOperator(api::ARCSINE, "arcsin");
+ addOperator(api::ARCCOSINE, "arccos");
+ addOperator(api::ARCTANGENT, "arctan");
+ addOperator(api::ARCCOSECANT, "arccsc");
+ addOperator(api::ARCSECANT, "arcsec");
+ addOperator(api::ARCCOTANGENT, "arccot");
+ addOperator(api::SQRT, "sqrt");
}
void Smt2::addQuantifiersOperators()
{
- if (!strictModeEnabled())
- {
- addOperator(kind::INST_CLOSURE, "inst-closure");
- }
}
void Smt2::addBitvectorOperators() {
- addOperator(kind::BITVECTOR_CONCAT, "concat");
- addOperator(kind::BITVECTOR_NOT, "bvnot");
- addOperator(kind::BITVECTOR_AND, "bvand");
- addOperator(kind::BITVECTOR_OR, "bvor");
- addOperator(kind::BITVECTOR_NEG, "bvneg");
- addOperator(kind::BITVECTOR_PLUS, "bvadd");
- addOperator(kind::BITVECTOR_MULT, "bvmul");
- addOperator(kind::BITVECTOR_UDIV, "bvudiv");
- addOperator(kind::BITVECTOR_UREM, "bvurem");
- addOperator(kind::BITVECTOR_SHL, "bvshl");
- addOperator(kind::BITVECTOR_LSHR, "bvlshr");
- addOperator(kind::BITVECTOR_ULT, "bvult");
- addOperator(kind::BITVECTOR_NAND, "bvnand");
- addOperator(kind::BITVECTOR_NOR, "bvnor");
- addOperator(kind::BITVECTOR_XOR, "bvxor");
- addOperator(kind::BITVECTOR_XNOR, "bvxnor");
- addOperator(kind::BITVECTOR_COMP, "bvcomp");
- addOperator(kind::BITVECTOR_SUB, "bvsub");
- addOperator(kind::BITVECTOR_SDIV, "bvsdiv");
- addOperator(kind::BITVECTOR_SREM, "bvsrem");
- addOperator(kind::BITVECTOR_SMOD, "bvsmod");
- addOperator(kind::BITVECTOR_ASHR, "bvashr");
- addOperator(kind::BITVECTOR_ULE, "bvule");
- addOperator(kind::BITVECTOR_UGT, "bvugt");
- addOperator(kind::BITVECTOR_UGE, "bvuge");
- addOperator(kind::BITVECTOR_SLT, "bvslt");
- addOperator(kind::BITVECTOR_SLE, "bvsle");
- addOperator(kind::BITVECTOR_SGT, "bvsgt");
- addOperator(kind::BITVECTOR_SGE, "bvsge");
- addOperator(kind::BITVECTOR_REDOR, "bvredor");
- addOperator(kind::BITVECTOR_REDAND, "bvredand");
- addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
-
+ addOperator(api::BITVECTOR_CONCAT, "concat");
+ addOperator(api::BITVECTOR_NOT, "bvnot");
+ addOperator(api::BITVECTOR_AND, "bvand");
+ addOperator(api::BITVECTOR_OR, "bvor");
+ addOperator(api::BITVECTOR_NEG, "bvneg");
+ addOperator(api::BITVECTOR_PLUS, "bvadd");
+ addOperator(api::BITVECTOR_MULT, "bvmul");
+ addOperator(api::BITVECTOR_UDIV, "bvudiv");
+ addOperator(api::BITVECTOR_UREM, "bvurem");
+ addOperator(api::BITVECTOR_SHL, "bvshl");
+ addOperator(api::BITVECTOR_LSHR, "bvlshr");
+ addOperator(api::BITVECTOR_ULT, "bvult");
+ addOperator(api::BITVECTOR_NAND, "bvnand");
+ addOperator(api::BITVECTOR_NOR, "bvnor");
+ addOperator(api::BITVECTOR_XOR, "bvxor");
+ addOperator(api::BITVECTOR_XNOR, "bvxnor");
+ addOperator(api::BITVECTOR_COMP, "bvcomp");
+ addOperator(api::BITVECTOR_SUB, "bvsub");
+ addOperator(api::BITVECTOR_SDIV, "bvsdiv");
+ addOperator(api::BITVECTOR_SREM, "bvsrem");
+ addOperator(api::BITVECTOR_SMOD, "bvsmod");
+ addOperator(api::BITVECTOR_ASHR, "bvashr");
+ addOperator(api::BITVECTOR_ULE, "bvule");
+ addOperator(api::BITVECTOR_UGT, "bvugt");
+ addOperator(api::BITVECTOR_UGE, "bvuge");
+ addOperator(api::BITVECTOR_SLT, "bvslt");
+ addOperator(api::BITVECTOR_SLE, "bvsle");
+ addOperator(api::BITVECTOR_SGT, "bvsgt");
+ addOperator(api::BITVECTOR_SGE, "bvsge");
+ addOperator(api::BITVECTOR_REDOR, "bvredor");
+ addOperator(api::BITVECTOR_REDAND, "bvredand");
+
+ addIndexedOperator(api::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
+ addIndexedOperator(api::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
addIndexedOperator(
- kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract");
+ api::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
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");
+ api::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
addIndexedOperator(
- kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv");
+ api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
+ addIndexedOperator(
+ api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "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(api::APPLY_CONSTRUCTOR);
+ Parser::addOperator(api::APPLY_TESTER);
+ Parser::addOperator(api::APPLY_SELECTOR);
if (!strictModeEnabled())
{
- addOperator(kind::DT_SIZE, "dt.size");
+ addOperator(api::DT_SIZE, "dt.size");
}
}
void Smt2::addStringOperators() {
- defineVar("re.all",
- getSolver()
- ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())
- .getExpr());
-
- addOperator(kind::STRING_CONCAT, "str.++");
- addOperator(kind::STRING_LENGTH, "str.len");
- addOperator(kind::STRING_SUBSTR, "str.substr" );
- addOperator(kind::STRING_STRCTN, "str.contains" );
- addOperator(kind::STRING_CHARAT, "str.at" );
- addOperator(kind::STRING_STRIDOF, "str.indexof" );
- addOperator(kind::STRING_STRREPL, "str.replace" );
- addOperator(kind::STRING_STRREPLALL, "str.replaceall");
+ defineVar(
+ "re.all",
+ getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma()));
+ addOperator(api::STRING_CONCAT, "str.++");
+ addOperator(api::STRING_LENGTH, "str.len");
+ addOperator(api::STRING_SUBSTR, "str.substr");
+ addOperator(api::STRING_CONTAINS, "str.contains");
+ addOperator(api::STRING_CHARAT, "str.at");
+ addOperator(api::STRING_INDEXOF, "str.indexof");
+ addOperator(api::STRING_REPLACE, "str.replace");
+ addOperator(api::STRING_PREFIX, "str.prefixof");
+ addOperator(api::STRING_SUFFIX, "str.suffixof");
+ addOperator(api::STRING_FROM_CODE, "str.from_code");
+ addOperator(api::STRING_IS_DIGIT, "str.is_digit");
+ addOperator(api::STRING_REPLACE_RE, "str.replace_re");
+ addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all");
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" );
- // 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");
+ addOperator(api::STRING_UPDATE, "str.update");
+ addOperator(api::STRING_TOLOWER, "str.tolower");
+ addOperator(api::STRING_TOUPPER, "str.toupper");
+ addOperator(api::STRING_REV, "str.rev");
+ // sequence versions
+ addOperator(api::SEQ_CONCAT, "seq.++");
+ addOperator(api::SEQ_LENGTH, "seq.len");
+ addOperator(api::SEQ_EXTRACT, "seq.extract");
+ addOperator(api::SEQ_UPDATE, "seq.update");
+ addOperator(api::SEQ_AT, "seq.at");
+ addOperator(api::SEQ_CONTAINS, "seq.contains");
+ addOperator(api::SEQ_INDEXOF, "seq.indexof");
+ addOperator(api::SEQ_REPLACE, "seq.replace");
+ addOperator(api::SEQ_PREFIX, "seq.prefixof");
+ addOperator(api::SEQ_SUFFIX, "seq.suffixof");
+ addOperator(api::SEQ_REV, "seq.rev");
+ addOperator(api::SEQ_REPLACE_ALL, "seq.replace_all");
+ addOperator(api::SEQ_UNIT, "seq.unit");
+ addOperator(api::SEQ_NTH, "seq.nth");
+ }
+ // at the moment, we only use this syntax for smt2.6
+ if (getLanguage() == language::input::LANG_SMTLIB_V2_6
+ || getLanguage() == language::input::LANG_SYGUS_V2)
+ {
+ addOperator(api::STRING_FROM_INT, "str.from_int");
+ addOperator(api::STRING_TO_INT, "str.to_int");
+ addOperator(api::STRING_IN_REGEXP, "str.in_re");
+ addOperator(api::STRING_TO_REGEXP, "str.to_re");
+ addOperator(api::STRING_TO_CODE, "str.to_code");
+ addOperator(api::STRING_REPLACE_ALL, "str.replace_all");
}
else
{
- addOperator(kind::STRING_ITOS, "int.to.str");
- addOperator(kind::STRING_STOI, "str.to.int");
- addOperator(kind::STRING_IN_REGEXP, "str.in.re");
- addOperator(kind::STRING_TO_REGEXP, "str.to.re");
- }
-
- addOperator(kind::REGEXP_CONCAT, "re.++");
- addOperator(kind::REGEXP_UNION, "re.union");
- addOperator(kind::REGEXP_INTER, "re.inter");
- addOperator(kind::REGEXP_STAR, "re.*");
- addOperator(kind::REGEXP_PLUS, "re.+");
- addOperator(kind::REGEXP_OPT, "re.opt");
- addOperator(kind::REGEXP_RANGE, "re.range");
- addOperator(kind::REGEXP_LOOP, "re.loop");
- addOperator(kind::STRING_CODE, "str.code");
- addOperator(kind::STRING_LT, "str.<");
- addOperator(kind::STRING_LEQ, "str.<=");
+ addOperator(api::STRING_FROM_INT, "int.to.str");
+ addOperator(api::STRING_TO_INT, "str.to.int");
+ addOperator(api::STRING_IN_REGEXP, "str.in.re");
+ addOperator(api::STRING_TO_REGEXP, "str.to.re");
+ addOperator(api::STRING_TO_CODE, "str.code");
+ addOperator(api::STRING_REPLACE_ALL, "str.replaceall");
+ }
+
+ addOperator(api::REGEXP_CONCAT, "re.++");
+ addOperator(api::REGEXP_UNION, "re.union");
+ addOperator(api::REGEXP_INTER, "re.inter");
+ addOperator(api::REGEXP_STAR, "re.*");
+ addOperator(api::REGEXP_PLUS, "re.+");
+ addOperator(api::REGEXP_OPT, "re.opt");
+ addIndexedOperator(api::REGEXP_REPEAT, api::REGEXP_REPEAT, "re.^");
+ addIndexedOperator(api::REGEXP_LOOP, api::REGEXP_LOOP, "re.loop");
+ addOperator(api::REGEXP_RANGE, "re.range");
+ addOperator(api::REGEXP_COMPLEMENT, "re.comp");
+ addOperator(api::REGEXP_DIFF, "re.diff");
+ addOperator(api::STRING_LT, "str.<");
+ addOperator(api::STRING_LEQ, "str.<=");
}
void Smt2::addFloatingPointOperators() {
- addOperator(kind::FLOATINGPOINT_FP, "fp");
- addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
- addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
- addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
- addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
- addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
- addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
- addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
- addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
- addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
- addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
- addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
- addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
- addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
- addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
- addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
- addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
- addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
- addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
- addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
- addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
- addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
- addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
- addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
- addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
- addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
-
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
- api::FLOATINGPOINT_TO_FP_GENERIC_OP,
+ addOperator(api::FLOATINGPOINT_FP, "fp");
+ addOperator(api::FLOATINGPOINT_EQ, "fp.eq");
+ addOperator(api::FLOATINGPOINT_ABS, "fp.abs");
+ addOperator(api::FLOATINGPOINT_NEG, "fp.neg");
+ addOperator(api::FLOATINGPOINT_PLUS, "fp.add");
+ addOperator(api::FLOATINGPOINT_SUB, "fp.sub");
+ addOperator(api::FLOATINGPOINT_MULT, "fp.mul");
+ addOperator(api::FLOATINGPOINT_DIV, "fp.div");
+ addOperator(api::FLOATINGPOINT_FMA, "fp.fma");
+ addOperator(api::FLOATINGPOINT_SQRT, "fp.sqrt");
+ addOperator(api::FLOATINGPOINT_REM, "fp.rem");
+ addOperator(api::FLOATINGPOINT_RTI, "fp.roundToIntegral");
+ addOperator(api::FLOATINGPOINT_MIN, "fp.min");
+ addOperator(api::FLOATINGPOINT_MAX, "fp.max");
+ addOperator(api::FLOATINGPOINT_LEQ, "fp.leq");
+ addOperator(api::FLOATINGPOINT_LT, "fp.lt");
+ addOperator(api::FLOATINGPOINT_GEQ, "fp.geq");
+ addOperator(api::FLOATINGPOINT_GT, "fp.gt");
+ addOperator(api::FLOATINGPOINT_ISN, "fp.isNormal");
+ addOperator(api::FLOATINGPOINT_ISSN, "fp.isSubnormal");
+ addOperator(api::FLOATINGPOINT_ISZ, "fp.isZero");
+ addOperator(api::FLOATINGPOINT_ISINF, "fp.isInfinite");
+ addOperator(api::FLOATINGPOINT_ISNAN, "fp.isNaN");
+ addOperator(api::FLOATINGPOINT_ISNEG, "fp.isNegative");
+ addOperator(api::FLOATINGPOINT_ISPOS, "fp.isPositive");
+ addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real");
+
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC,
+ api::FLOATINGPOINT_TO_FP_GENERIC,
"to_fp");
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
- api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+ api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
"to_fp_unsigned");
addIndexedOperator(
- kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv");
+ api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
addIndexedOperator(
- kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv");
+ api::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
if (!strictModeEnabled())
{
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
- api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+ api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
"to_fp_bv");
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
- api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+ api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
"to_fp_fp");
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
- api::FLOATINGPOINT_TO_FP_REAL_OP,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL,
+ api::FLOATINGPOINT_TO_FP_REAL,
"to_fp_real");
- addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
- api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
+ addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+ api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
"to_fp_signed");
}
}
void Smt2::addSepOperators() {
- addOperator(kind::SEP_STAR, "sep");
- addOperator(kind::SEP_PTO, "pto");
- addOperator(kind::SEP_WAND, "wand");
- addOperator(kind::SEP_EMP, "emp");
- Parser::addOperator(kind::SEP_STAR);
- Parser::addOperator(kind::SEP_PTO);
- Parser::addOperator(kind::SEP_WAND);
- Parser::addOperator(kind::SEP_EMP);
+ addOperator(api::SEP_STAR, "sep");
+ addOperator(api::SEP_PTO, "pto");
+ addOperator(api::SEP_WAND, "wand");
+ addOperator(api::SEP_EMP, "emp");
+ Parser::addOperator(api::SEP_STAR);
+ Parser::addOperator(api::SEP_PTO);
+ Parser::addOperator(api::SEP_WAND);
+ Parser::addOperator(api::SEP_EMP);
}
-void Smt2::addTheory(Theory theory) {
- switch(theory) {
- case THEORY_ARRAYS:
- addOperator(kind::SELECT, "select");
- addOperator(kind::STORE, "store");
- break;
-
- case THEORY_BITVECTORS:
- addBitvectorOperators();
- break;
-
- case THEORY_CORE:
- defineType("Bool", getExprManager()->booleanType());
- defineVar("true", getExprManager()->mkConst(true));
- defineVar("false", getExprManager()->mkConst(false));
- addOperator(kind::AND, "and");
- addOperator(kind::DISTINCT, "distinct");
- addOperator(kind::EQUAL, "=");
- addOperator(kind::IMPLIES, "=>");
- addOperator(kind::ITE, "ite");
- addOperator(kind::NOT, "not");
- addOperator(kind::OR, "or");
- addOperator(kind::XOR, "xor");
- break;
-
- case THEORY_REALS_INTS:
- defineType("Real", getExprManager()->realType());
- addOperator(kind::DIVISION, "/");
- addOperator(kind::TO_INTEGER, "to_int");
- addOperator(kind::IS_INTEGER, "is_int");
- addOperator(kind::TO_REAL, "to_real");
- // falling through on purpose, to add Ints part of Reals_Ints
- case THEORY_INTS:
- defineType("Int", getExprManager()->integerType());
- addArithmeticOperators();
- addOperator(kind::INTS_DIVISION, "div");
- addOperator(kind::INTS_MODULUS, "mod");
- addOperator(kind::ABS, "abs");
- addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible");
- break;
-
- case THEORY_REALS:
- defineType("Real", getExprManager()->realType());
- addArithmeticOperators();
- addOperator(kind::DIVISION, "/");
- if (!strictModeEnabled())
- {
- addOperator(kind::ABS, "abs");
- }
- break;
-
- 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::SUBSET, "subset");
- addOperator(kind::MEMBER, "member");
- addOperator(kind::SINGLETON, "singleton");
- addOperator(kind::INSERT, "insert");
- addOperator(kind::CARD, "card");
- addOperator(kind::COMPLEMENT, "complement");
- addOperator(kind::JOIN, "join");
- addOperator(kind::PRODUCT, "product");
- addOperator(kind::TRANSPOSE, "transpose");
- addOperator(kind::TCLOSURE, "tclosure");
- break;
-
- case THEORY_DATATYPES:
- {
- 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("RoundingMode", getExprManager()->roundingModeType());
- defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
- defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
- defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
- defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
-
- defineVar(
- "RNE",
- d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
- defineVar(
- "roundNearestTiesToEven",
- d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
- defineVar(
- "RNA",
- d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
- defineVar(
- "roundNearestTiesToAway",
- d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
- defineVar("RTP",
- d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
- 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;
-
- default:
- std::stringstream ss;
- ss << "internal error: unsupported theory " << theory;
- throw ParserException(ss.str());
- }
+void Smt2::addCoreSymbols()
+{
+ defineType("Bool", d_solver->getBooleanSort(), true, true);
+ defineVar("true", d_solver->mkTrue(), true, true);
+ defineVar("false", d_solver->mkFalse(), true, true);
+ addOperator(api::AND, "and");
+ addOperator(api::DISTINCT, "distinct");
+ addOperator(api::EQUAL, "=");
+ addOperator(api::IMPLIES, "=>");
+ addOperator(api::ITE, "ite");
+ addOperator(api::NOT, "not");
+ addOperator(api::OR, "or");
+ addOperator(api::XOR, "xor");
}
-void Smt2::addOperator(Kind kind, const std::string& name) {
+void Smt2::addOperator(api::Kind kind, const std::string& name)
+{
Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
<< std::endl;
Parser::addOperator(kind);
operatorKindMap[name] = kind;
}
-void Smt2::addIndexedOperator(Kind tKind,
+void Smt2::addIndexedOperator(api::Kind tKind,
api::Kind opKind,
const std::string& name)
{
d_indexedOpKindMap[name] = opKind;
}
-Kind Smt2::getOperatorKind(const std::string& name) const {
+api::Kind Smt2::getOperatorKind(const std::string& name) const
+{
// precondition: isOperatorEnabled(name)
return operatorKindMap.find(name)->second;
}
return operatorKindMap.find(name) != operatorKindMap.end();
}
-bool Smt2::isTheoryEnabled(Theory theory) const {
- switch(theory) {
- case THEORY_ARRAYS:
- return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
- case THEORY_BITVECTORS:
- return d_logic.isTheoryEnabled(theory::THEORY_BV);
- case THEORY_CORE:
- return true;
- case THEORY_DATATYPES:
- return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
- case THEORY_INTS:
- return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
- d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
- case THEORY_REALS:
- return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
- ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
- case THEORY_REALS_INTS:
- return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
- d_logic.areIntegersUsed() && d_logic.areRealsUsed();
- case THEORY_QUANTIFIERS:
- return d_logic.isQuantified();
- case THEORY_SETS:
- return d_logic.isTheoryEnabled(theory::THEORY_SETS);
- case THEORY_STRINGS:
- return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
- case THEORY_UF:
- return d_logic.isTheoryEnabled(theory::THEORY_UF);
- case THEORY_FP:
- return d_logic.isTheoryEnabled(theory::THEORY_FP);
- case THEORY_SEP:
- return d_logic.isTheoryEnabled(theory::THEORY_SEP);
- default:
- std::stringstream ss;
- ss << "internal error: unsupported theory " << theory;
- throw ParserException(ss.str());
- }
+bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
+{
+ return d_logic.isTheoryEnabled(theory);
+}
+
+bool Smt2::isHoEnabled() const
+{
+ return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo();
}
bool Smt2::logicIsSet() {
return d_logicSet;
}
-Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
+api::Term Smt2::getExpressionForNameAndType(const std::string& name,
+ api::Sort t)
+{
if (isAbstractValue(name))
{
return mkAbstractValue(name);
return Parser::getExpressionForNameAndType(name, t);
}
+bool Smt2::getTesterName(api::Term cons, std::string& name)
+{
+ if ((v2_6() || sygus_v2()) && strictModeEnabled())
+ {
+ // 2.6 or above uses indexed tester symbols, if we are in strict mode,
+ // we do not automatically define is-cons for constructor cons.
+ return false;
+ }
+ std::stringstream ss;
+ ss << "is-" << cons;
+ name = ss.str();
+ return true;
+}
+
api::Term Smt2::mkIndexedConstant(const std::string& name,
const std::vector<uint64_t>& numerals)
{
- if (isTheoryEnabled(THEORY_FP))
+ if (d_logic.isTheoryEnabled(theory::THEORY_FP))
{
if (name == "+oo")
{
}
}
- if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0)
+ if (d_logic.isTheoryEnabled(theory::THEORY_BV) && name.find("bv") == 0)
{
std::string bvStr = name.substr(2);
return d_solver->mkBitVector(numerals[0], bvStr, 10);
return api::Term();
}
-api::OpTerm Smt2::mkIndexedOp(const std::string& name,
- const std::vector<uint64_t>& numerals)
+api::Op 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]);
+ return d_solver->mkOp(k, numerals[0]);
}
else if (numerals.size() == 2)
{
- return d_solver->mkOpTerm(k, numerals[0], numerals[1]);
+ return d_solver->mkOp(k, numerals[0], numerals[1]);
}
}
parseError(std::string("Unknown indexed function `") + name + "'");
- return api::OpTerm();
+ return api::Op();
}
-Expr Smt2::mkDefineFunRec(
+api::Term Smt2::bindDefineFunRec(
const std::string& fname,
- const std::vector<std::pair<std::string, Type> >& sortedVarNames,
- Type t,
- std::vector<Expr>& flattenVars)
+ const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
+ api::Sort t,
+ std::vector<api::Term>& flattenVars)
{
- std::vector<Type> sorts;
- for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
+ std::vector<api::Sort> sorts;
+ for (const std::pair<std::string, api::Sort>& svn : sortedVarNames)
{
sorts.push_back(svn.second);
}
// make the flattened function type, add bound variables
// to flattenVars if the defined function was given a function return type.
- Type ft = mkFlatFunctionType(sorts, t, flattenVars);
+ api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars);
// allow overloading
- return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
+ return bindVar(fname, ft, false, 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)
+ const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
+ api::Term func,
+ const std::vector<api::Term>& flattenVars,
+ std::vector<api::Term>& bvs)
{
- pushScope(bindingLevel);
+ pushScope();
// bound variables are those that are explicitly named in the preamble
// of the define-fun(s)-rec command, we define them here
- for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
+ for (const std::pair<std::string, api::Sort>& svn : sortedVarNames)
{
- Expr v = mkBoundVar(svn.first, svn.second);
+ api::Term v = bindBoundVar(svn.first, svn.second);
bvs.push_back(v);
}
d_seenSetLogic = false;
d_logic = LogicInfo();
operatorKindMap.clear();
- d_lastNamedTerm = std::pair<Expr, std::string>();
- this->Parser::reset();
-
- if( !strictModeEnabled() ) {
- addTheory(Smt2::THEORY_CORE);
- }
-}
-
-void Smt2::resetAssertions() {
- // Remove all declarations except the ones at level 0.
- while (this->scopeLevel() > 0) {
- this->popScope();
- }
-}
-
-std::unique_ptr<Command> Smt2::assertRewriteRule(
- Kind kind,
- Expr bvl,
- const std::vector<Expr>& triggers,
- const std::vector<Expr>& guards,
- const std::vector<Expr>& heads,
- Expr body)
-{
- assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION
- || kind == kind::RR_DEDUCTION);
-
- ExprManager* em = getExprManager();
-
- std::vector<Expr> args;
- args.push_back(mkAnd(heads));
- args.push_back(body);
-
- if (!triggers.empty())
- {
- args.push_back(em->mkExpr(kind::INST_PATTERN_LIST, triggers));
- }
-
- Expr rhs = em->mkExpr(kind, args);
- Expr rule = em->mkExpr(kind::REWRITE_RULE, bvl, mkAnd(guards), rhs);
- return std::unique_ptr<Command>(new AssertCommand(rule, false));
-}
-
-Smt2::SynthFunFactory::SynthFunFactory(
- Smt2* smt2,
- const std::string& fun,
- bool isInv,
- Type range,
- std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames)
- : d_smt2(smt2), d_fun(fun), d_isInv(isInv)
-{
- if (range.isNull())
- {
- smt2->parseError("Must supply return type for synth-fun.");
- }
- if (range.isFunction())
- {
- smt2->parseError("Cannot use synth-fun with function return type.");
- }
- std::vector<Type> varSorts;
- for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
- {
- varSorts.push_back(p.second);
- }
- Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
- Type synthFunType =
- varSorts.size() > 0
- ? d_smt2->getExprManager()->mkFunctionType(varSorts, range)
- : range;
-
- // we do not allow overloading for synth fun
- d_synthFun = d_smt2->mkBoundVar(fun, synthFunType);
- // set the sygus type to be range by default, which is overwritten below
- // if a grammar is provided
- d_sygusType = range;
-
- d_smt2->pushScope(true);
- d_sygusVars = d_smt2->mkBoundVars(sortedVarNames);
-}
-
-Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
-
-std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(Type grammar)
-{
- Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
- return std::unique_ptr<Command>(
- new SynthFunCommand(d_fun,
- d_synthFun,
- grammar.isNull() ? d_sygusType : grammar,
- d_isInv,
- d_sygusVars));
+ d_lastNamedTerm = std::pair<api::Term, std::string>();
}
std::unique_ptr<Command> Smt2::invConstraint(
"arguments.");
}
- std::vector<Expr> terms;
+ std::vector<api::Term> terms;
for (const std::string& name : names)
{
if (!isDeclared(name))
}
}
- 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";
- }else if(name == "Reals") {
- name = "LRA";
- }
- }
-
d_logicSet = true;
d_logic = name;
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
- addTheory(THEORY_CORE);
+ addCoreSymbols();
if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
- addTheory(THEORY_UF);
+ Parser::addOperator(api::APPLY_UF);
+
+ if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
+ {
+ addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card");
+ addOperator(api::CARDINALITY_VALUE, "fmf.card.val");
+ }
}
if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
if(d_logic.areIntegersUsed()) {
- if(d_logic.areRealsUsed()) {
- addTheory(THEORY_REALS_INTS);
- } else {
- addTheory(THEORY_INTS);
+ defineType("Int", d_solver->getIntegerSort(), true, true);
+ addArithmeticOperators();
+ if (!strictModeEnabled() || !d_logic.isLinear())
+ {
+ addOperator(api::INTS_DIVISION, "div");
+ addOperator(api::INTS_MODULUS, "mod");
+ addOperator(api::ABS, "abs");
}
- } else if(d_logic.areRealsUsed()) {
- addTheory(THEORY_REALS);
+ addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible");
+ }
+
+ if (d_logic.areRealsUsed())
+ {
+ defineType("Real", d_solver->getRealSort(), true, true);
+ addArithmeticOperators();
+ addOperator(api::DIVISION, "/");
+ if (!strictModeEnabled())
+ {
+ addOperator(api::ABS, "abs");
+ }
+ }
+
+ if (d_logic.areIntegersUsed() && d_logic.areRealsUsed())
+ {
+ addOperator(api::TO_INTEGER, "to_int");
+ addOperator(api::IS_INTEGER, "is_int");
+ addOperator(api::TO_REAL, "to_real");
}
if (d_logic.areTranscendentalsUsed())
{
- addTheory(THEORY_TRANSCENDENTALS);
+ defineVar("real.pi", d_solver->mkTerm(api::PI));
+ addTranscendentalOperators();
+ }
+ if (!strictModeEnabled())
+ {
+ // integer version of AND
+ addIndexedOperator(api::IAND, api::IAND, "iand");
}
}
if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
- addTheory(THEORY_ARRAYS);
+ addOperator(api::SELECT, "select");
+ addOperator(api::STORE, "store");
+ addOperator(api::EQ_RANGE, "eqrange");
}
if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
- addTheory(THEORY_BITVECTORS);
+ addBitvectorOperators();
+
+ if (!strictModeEnabled() && d_logic.isTheoryEnabled(theory::THEORY_ARITH)
+ && d_logic.areIntegersUsed())
+ {
+ // Conversions between bit-vectors and integers
+ addOperator(api::BITVECTOR_TO_NAT, "bv2nat");
+ addIndexedOperator(
+ api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
+ }
}
if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
- addTheory(THEORY_DATATYPES);
+ const std::vector<api::Sort> types;
+ defineType("Tuple", d_solver->mkTupleSort(types), true, true);
+ addDatatypesOperators();
}
if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
- addTheory(THEORY_SETS);
+ defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort()));
+ // the Boolean sort is a placeholder here since we don't have type info
+ // without type annotation
+ defineVar("univset", d_solver->mkUniverseSet(d_solver->getBooleanSort()));
+
+ addOperator(api::UNION, "union");
+ addOperator(api::INTERSECTION, "intersection");
+ addOperator(api::SETMINUS, "setminus");
+ addOperator(api::SUBSET, "subset");
+ addOperator(api::MEMBER, "member");
+ addOperator(api::SINGLETON, "singleton");
+ addOperator(api::INSERT, "insert");
+ addOperator(api::CARD, "card");
+ addOperator(api::COMPLEMENT, "complement");
+ addOperator(api::CHOOSE, "choose");
+ addOperator(api::IS_SINGLETON, "is_singleton");
+ addOperator(api::JOIN, "join");
+ addOperator(api::PRODUCT, "product");
+ addOperator(api::TRANSPOSE, "transpose");
+ addOperator(api::TCLOSURE, "tclosure");
+ }
+
+ if (d_logic.isTheoryEnabled(theory::THEORY_BAGS))
+ {
+ defineVar("emptybag", d_solver->mkEmptyBag(d_solver->getNullSort()));
+ addOperator(api::UNION_MAX, "union_max");
+ addOperator(api::UNION_DISJOINT, "union_disjoint");
+ addOperator(api::INTERSECTION_MIN, "intersection_min");
+ addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract");
+ addOperator(api::DIFFERENCE_REMOVE, "difference_remove");
+ addOperator(api::SUBBAG, "subbag");
+ addOperator(api::BAG_COUNT, "bag.count");
+ addOperator(api::DUPLICATE_REMOVAL, "duplicate_removal");
+ addOperator(api::MK_BAG, "bag");
+ addOperator(api::BAG_CARD, "bag.card");
+ addOperator(api::BAG_CHOOSE, "bag.choose");
+ addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton");
+ addOperator(api::BAG_FROM_SET, "bag.from_set");
+ addOperator(api::BAG_TO_SET, "bag.to_set");
}
-
if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
- addTheory(THEORY_STRINGS);
+ defineType("String", d_solver->getStringSort(), true, true);
+ defineType("RegLan", d_solver->getRegExpSort(), true, true);
+ defineType("Int", d_solver->getIntegerSort(), true, true);
+
+ if (getLanguage() == language::input::LANG_SMTLIB_V2_6
+ || getLanguage() == language::input::LANG_SYGUS_V2)
+ {
+ defineVar("re.none", d_solver->mkRegexpEmpty());
+ }
+ else
+ {
+ defineVar("re.nostr", d_solver->mkRegexpEmpty());
+ }
+ defineVar("re.allchar", d_solver->mkRegexpSigma());
+
+ // Boolean is a placeholder
+ defineVar("seq.empty",
+ d_solver->mkEmptySequence(d_solver->getBooleanSort()));
+
+ addStringOperators();
}
if(d_logic.isQuantified()) {
- addTheory(THEORY_QUANTIFIERS);
+ addQuantifiersOperators();
}
if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
- addTheory(THEORY_FP);
+ defineType("RoundingMode", d_solver->getRoundingModeSort(), true, true);
+ defineType("Float16", d_solver->mkFloatingPointSort(5, 11), true, true);
+ defineType("Float32", d_solver->mkFloatingPointSort(8, 24), true, true);
+ defineType("Float64", d_solver->mkFloatingPointSort(11, 53), true, true);
+ defineType("Float128", d_solver->mkFloatingPointSort(15, 113), true, true);
+
+ defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
+ defineVar("roundNearestTiesToEven",
+ d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
+ defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
+ defineVar("roundNearestTiesToAway",
+ d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
+ defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
+ defineVar("roundTowardPositive",
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
+ defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
+ defineVar("roundTowardNegative",
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
+ defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
+ defineVar("roundTowardZero",
+ d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
+
+ addFloatingPointOperators();
}
if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
- addTheory(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()));
+
+ addSepOperators();
}
Command* cmd =
return cmd;
} /* 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
+api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
+ const std::vector<api::Term>& ntSymbols)
{
- return getLanguage() == language::input::LANG_SYGUS;
+ d_allocGrammars.emplace_back(
+ new api::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols)));
+ return d_allocGrammars.back().get();
}
-void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
- // TODO: ???
+bool Smt2::sygus() const
+{
+ InputLanguage ilang = getLanguage();
+ return ilang == language::input::LANG_SYGUS_V2;
}
-void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
- // TODO: ???
+bool Smt2::sygus_v2() const
+{
+ return getLanguage() == language::input::LANG_SYGUS_V2;
}
void Smt2::checkThatLogicIsSet()
}
}
+void Smt2::checkLogicAllowsFreeSorts()
+{
+ if (!d_logic.isTheoryEnabled(theory::THEORY_UF)
+ && !d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)
+ && !d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)
+ && !d_logic.isTheoryEnabled(theory::THEORY_SETS)
+ && !d_logic.isTheoryEnabled(theory::THEORY_BAGS))
+ {
+ parseErrorLogic("Free sort symbols not allowed in ");
+ }
+}
+
+void Smt2::checkLogicAllowsFunctions()
+{
+ if (!d_logic.isTheoryEnabled(theory::THEORY_UF))
+ {
+ parseError(
+ "Functions (of non-zero arity) cannot "
+ "be declared in logic "
+ + d_logic.getLogicString() + " unless option --uf-ho is used");
+ }
+}
+
/* The include are managed in the lexer but called in the parser */
// Inspired by http://www.antlr3.org/api/C/interop.html
parseError("Couldn't open include file `" + path + "'");
}
}
-
-void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
- if( type.isInteger() ){
- ops.push_back(getExprManager()->mkConst(Rational(0)));
- ops.push_back(getExprManager()->mkConst(Rational(1)));
- }else if( type.isBitVector() ){
- unsigned sz = ((BitVectorType)type).getSize();
- BitVector bval0(sz, (unsigned int)0);
- ops.push_back( getExprManager()->mkConst(bval0) );
- BitVector bval1(sz, (unsigned int)1);
- ops.push_back( getExprManager()->mkConst(bval1) );
- }else if( type.isBoolean() ){
- ops.push_back(getExprManager()->mkConst(true));
- ops.push_back(getExprManager()->mkConst(false));
- }
- //TODO : others?
-}
-
-// This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
-// This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
-void Smt2::processSygusGTerm(
- CVC4::SygusGTerm& sgt,
- int index,
- std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
- std::vector<std::vector<CVC4::Expr>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- const std::vector<CVC4::Expr>& sygus_vars,
- std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
- std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
- CVC4::Type& ret,
- bool isNested)
-{
- if (sgt.d_gterm_type == SygusGTerm::gterm_op)
- {
- Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
- << std::endl;
- Kind oldKind;
- Kind newKind = kind::UNDEFINED_KIND;
- //convert to UMINUS if one child of MINUS
- if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
- oldKind = kind::MINUS;
- newKind = kind::UMINUS;
- }
- if( newKind!=kind::UNDEFINED_KIND ){
- Expr newExpr = getExprManager()->operatorOf(newKind);
- Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
- sgt.d_expr = newExpr;
- std::string oldName = kind::kindToString(oldKind);
- std::string newName = kind::kindToString(newKind);
- size_t pos = 0;
- if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
- sgt.d_name.replace(pos, oldName.length(), newName);
- }
- }
- ops[index].push_back( sgt.d_expr );
- cnames[index].push_back( sgt.d_name );
- cargs[index].push_back( std::vector< CVC4::Type >() );
- for( unsigned i=0; i<sgt.d_children.size(); i++ ){
- std::stringstream ss;
- ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
- std::string sub_dname = ss.str();
- //add datatype for child
- Type null_type;
- pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- int sub_dt_index = datatypes.size()-1;
- //process child
- Type sub_ret;
- processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
- sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
- //process the nested gterm (either pop the last datatype, or flatten the argument)
- Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
- sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
- cargs[index].back().push_back(tt);
- }
- }
- else if (sgt.d_gterm_type == SygusGTerm::gterm_constant)
- {
- if( sgt.getNumChildren()!=0 ){
- parseError("Bad syntax for Sygus Constant.");
- }
- std::vector< Expr > consts;
- mkSygusConstantsForType( sgt.d_type, consts );
- Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
- for( unsigned i=0; i<consts.size(); i++ ){
- std::stringstream ss;
- ss << consts[i];
- Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
- ops[index].push_back( consts[i] );
- cnames[index].push_back( ss.str() );
- cargs[index].push_back( std::vector< CVC4::Type >() );
- }
- allow_const[index] = true;
- }
- else if (sgt.d_gterm_type == SygusGTerm::gterm_variable
- || sgt.d_gterm_type == SygusGTerm::gterm_input_variable)
- {
- if( sgt.getNumChildren()!=0 ){
- parseError("Bad syntax for Sygus Variable.");
- }
- Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
- for( unsigned i=0; i<sygus_vars.size(); i++ ){
- if( sygus_vars[i].getType()==sgt.d_type ){
- std::stringstream ss;
- ss << sygus_vars[i];
- Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
- ops[index].push_back( sygus_vars[i] );
- cnames[index].push_back( ss.str() );
- cargs[index].push_back( std::vector< CVC4::Type >() );
- }
- }
- }
- else if (sgt.d_gterm_type == SygusGTerm::gterm_nested_sort)
- {
- ret = sgt.d_type;
- }
- else if (sgt.d_gterm_type == SygusGTerm::gterm_unresolved)
- {
- if( isNested ){
- if( isUnresolvedType(sgt.d_name) ){
- ret = getSort(sgt.d_name);
- }else{
- //nested, unresolved symbol...fail
- std::stringstream ss;
- ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
- parseError(ss.str());
- }
- }else{
- //will resolve when adding constructors
- unresolved_gterm_sym[index].push_back(sgt.d_name);
- }
- }
- else if (sgt.d_gterm_type == SygusGTerm::gterm_ignore)
- {
- // do nothing
- }
-}
-
-bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
- std::vector< CVC4::Datatype >& datatypes,
- std::vector< CVC4::Type>& sorts,
- std::vector< std::vector<CVC4::Expr> >& ops,
- std::vector< std::vector<std::string> >& cnames,
- std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
- std::vector< bool >& allow_const,
- std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
- sorts.push_back(t);
- datatypes.push_back(Datatype(dname));
- ops.push_back(std::vector<Expr>());
- cnames.push_back(std::vector<std::string>());
- cargs.push_back(std::vector<std::vector<CVC4::Type> >());
- allow_const.push_back(false);
- unresolved_gterm_sym.push_back(std::vector< std::string >());
- return true;
-}
-
-bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
- std::vector< CVC4::Type>& sorts,
- std::vector< std::vector<CVC4::Expr> >& ops,
- std::vector< std::vector<std::string> >& cnames,
- std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
- std::vector< bool >& allow_const,
- std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
- sorts.pop_back();
- datatypes.pop_back();
- ops.pop_back();
- cnames.pop_back();
- cargs.pop_back();
- allow_const.pop_back();
- unresolved_gterm_sym.pop_back();
- return true;
-}
-
-Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
- std::vector< CVC4::Type>& sorts,
- std::vector< std::vector<CVC4::Expr> >& ops,
- std::vector< std::vector<std::string> >& cnames,
- std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
- std::vector< bool >& allow_const,
- std::vector< std::vector< std::string > >& unresolved_gterm_sym,
- std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
- std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
- Type t = sub_ret;
- Debug("parser-sygus") << "Argument is ";
- if( t.isNull() ){
- //then, it is the datatype we constructed, which should have a single constructor
- t = mkUnresolvedType(sub_dname);
- Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl;
- Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl;
- if( cargs[sub_dt_index].empty() ){
- parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
- }
- Expr sop = ops[sub_dt_index][0];
- Type curr_t;
- 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;
- // 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;
- if( sop.getKind() != kind::BUILTIN ){
- children.push_back( sop );
- }
- for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
- std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
- if( it==sygus_to_builtin_expr.end() ){
- if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
- std::stringstream ss;
- ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
- ss << "Builtin types are currently : " << std::endl;
- for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
- ss << " " << itb->first << " -> " << itb->second << std::endl;
- }
- parseError(ss.str());
- }
- Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
- Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
- std::stringstream ss;
- ss << t << "_x_" << i;
- Expr bv = mkBoundVar(ss.str(), bt);
- children.push_back( bv );
- d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
- }else{
- Debug("parser-sygus") << ": child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
- children.push_back( it->second );
- }
- }
- 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;
- curr_t = e.getType();
- sygus_to_builtin_expr[t] = e;
- }
- sorts[sub_dt_index] = curr_t;
- sygus_to_builtin[t] = curr_t;
- }else{
- Debug("parser-sygus") << "simple argument " << t << std::endl;
- Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
- //otherwise, datatype was unecessary
- //pop argument datatype definition
- popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- }
- return t;
-}
-
-void Smt2::setSygusStartIndex(const std::string& fun,
- int startIndex,
- std::vector<CVC4::Datatype>& datatypes,
- std::vector<CVC4::Type>& sorts,
- std::vector<std::vector<CVC4::Expr>>& ops)
-{
- if( startIndex>0 ){
- CVC4::Datatype tmp_dt = datatypes[0];
- Type tmp_sort = sorts[0];
- std::vector< Expr > tmp_ops;
- tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
- datatypes[0] = datatypes[startIndex];
- sorts[0] = sorts[startIndex];
- ops[0].clear();
- ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
- datatypes[startIndex] = tmp_dt;
- sorts[startIndex] = tmp_sort;
- ops[startIndex].clear();
- ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
- }else if( startIndex<0 ){
- std::stringstream ss;
- ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
- warning(ss.str());
- }
-}
-
-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;
-
- 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;
- for (unsigned j = 0; j < i; j++)
- {
- if( ops[i]==ops[j] ){
- is_dup_op = true;
- if( cargs[i].size()==cargs[j].size() ){
- is_dup = true;
- for( unsigned k=0; k<cargs[i].size(); k++ ){
- if( cargs[i][k]!=cargs[j][k] ){
- is_dup = false;
- break;
- }
- }
- }
- if( is_dup ){
- break;
- }
- }
- }
- Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
- if( is_dup ){
- 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
- {
- 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);
- }
- 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 (ops[i].getKind() == kind::VARIABLE)
- {
- Debug("parser-sygus") << "--> Defined function " << ops[i]
- << std::endl;
- // turn f into (lammbda (x) (f x))
- // in a degenerate case, ops[i] may be a defined constant,
- // in which case we do not replace by a lambda.
- if (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;
- }
- }
- // must rename to avoid duplication
- std::stringstream ss;
- ss << dt.getName() << "_" << i << "_" << cnames[i];
- cnames[i] = ss.str();
- 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;
- Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
- for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
- Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym[i] << std::endl;
- if( isUnresolvedType(unresolved_gterm_sym[i]) ){
- Debug("parser-sygus") << " it is an unresolved type." << std::endl;
- Type t = getSort(unresolved_gterm_sym[i]);
- if( std::find( types.begin(), types.end(), t )==types.end() ){
- types.push_back( t );
- //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";
- 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, sepc);
-
- //add to operators
- ops.push_back( id_op );
- }
- }else{
- std::stringstream ss;
- ss << "Unhandled sygus constructor " << unresolved_gterm_sym[i];
- throw ParserException(ss.str());
- }
- }
- }
-}
-
-Expr Smt2::makeSygusBoundVarList(Datatype& dt,
- unsigned i,
- const std::vector<Type>& ltypes,
- std::vector<Expr>& lvars)
+bool Smt2::isAbstractValue(const std::string& name)
{
- 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);
+ return name.length() >= 2 && name[0] == '@' && name[1] != '0'
+ && name.find_first_not_of("0123456789", 1) == std::string::npos;
}
-void Smt2::addSygusConstructorTerm(Datatype& dt,
- Expr term,
- std::map<Expr, Type>& ntsToUnres) const
+api::Term Smt2::mkAbstractValue(const std::string& name)
{
- 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;
- }
- }
- }
- 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 is parameterized. This includes APPLY_UF terms and BV
- // extraction terms, but excludes applications of most interpreted symbols
- // like PLUS.
- if (term.isParameterized())
- {
- 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,
- const 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);
- }
- }
+ assert(isAbstractValue(name));
+ // remove the '@'
+ return d_solver->mkAbstractValue(name.substr(1));
}
InputLanguage Smt2::getLanguage() const
{
- ExprManager* em = getExprManager();
- return em->getOptions().getInputLanguage();
+ return d_solver->getOptions().getInputLanguage();
}
-void Smt2::applyTypeAscription(ParseOp& p, Type type)
+void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
{
+ Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
+ << std::endl;
// (as const (Array T1 T2))
- if (p.d_kind == kind::STORE_ALL)
+ if (p.d_kind == api::CONST_ARRAY)
{
if (!type.isArray())
{
if (isDeclared(p.d_name, SYM_VARIABLE))
{
p.d_expr = getExpressionForNameAndType(p.d_name, type);
+ p.d_name = std::string("");
}
if (p.d_expr.isNull())
{
parseError(ss.str());
}
}
- ExprManager* em = getExprManager();
- Type etype = p.d_expr.getType();
- Kind ekind = p.d_expr.getKind();
Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
- Trace("parser-qid") << " " << ekind << " " << etype;
+ Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort();
Trace("parser-qid") << std::endl;
- if (ekind == kind::APPLY_CONSTRUCTOR && type.isDatatype())
- {
- // nullary constructors with a type ascription
- // could be a parametric constructor or just an overloaded constructor
- DatatypeType dtype = static_cast<DatatypeType>(type);
- if (dtype.isParametric())
- {
- std::vector<Expr> v;
- Expr e = p.d_expr.getOperator();
- const DatatypeConstructor& dtc =
- Datatype::datatypeOf(e)[Datatype::indexOf(e)];
- v.push_back(em->mkExpr(
- kind::APPLY_TYPE_ASCRIPTION,
- em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
- p.d_expr.getOperator()));
- v.insert(v.end(), p.d_expr.begin(), p.d_expr.end());
- p.d_expr = em->mkExpr(kind::APPLY_CONSTRUCTOR, v);
- }
- }
- else if (etype.isConstructor())
- {
- // a non-nullary constructor with a type ascription
- DatatypeType dtype = static_cast<DatatypeType>(type);
- if (dtype.isParametric())
- {
- const DatatypeConstructor& dtc =
- Datatype::datatypeOf(p.d_expr)[Datatype::indexOf(p.d_expr)];
- p.d_expr = em->mkExpr(
- kind::APPLY_TYPE_ASCRIPTION,
- em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
- p.d_expr);
- }
- }
- else if (ekind == kind::EMPTYSET)
- {
- Debug("parser") << "Empty set encountered: " << p.d_expr << " " << type
- << std::endl;
- p.d_expr = em->mkConst(EmptySet(type));
- }
- else if (ekind == kind::UNIVERSE_SET)
- {
- p.d_expr = em->mkNullaryOperator(type, kind::UNIVERSE_SET);
- }
- else if (ekind == kind::SEP_NIL)
- {
- // We don't want the nil reference to be a constant: for instance, it
- // could be of type Int but is not a const rational. However, the
- // expression has 0 children. So we convert to a SEP_NIL variable.
- p.d_expr = em->mkNullaryOperator(type, kind::SEP_NIL);
- }
- else if (etype != type)
- {
- parseError("Type ascription not satisfied.");
- }
+ // otherwise, we process the type ascription
+ p.d_expr = applyTypeAscription(p.d_expr, type);
}
-Expr Smt2::parseOpToExpr(ParseOp& p)
+api::Term Smt2::parseOpToExpr(ParseOp& p)
{
- Expr expr;
- if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull())
+ Debug("parser") << "parseOpToExpr: " << p << std::endl;
+ api::Term expr;
+ if (p.d_kind != api::NULL_EXPR || !p.d_type.isNull())
{
parseError(
"Bad syntax for qualified identifier operator in term position.");
}
else if (!isDeclared(p.d_name, SYM_VARIABLE))
{
- if (sygus_v1() && p.d_name[0] == '-'
- && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos)
- {
- // allow unary minus in sygus version 1
- expr = getExprManager()->mkConst(Rational(p.d_name));
- }
- else
- {
- std::stringstream ss;
- ss << "Symbol " << p.d_name << " is not declared.";
- parseError(ss.str());
- }
+ std::stringstream ss;
+ ss << "Symbol " << p.d_name << " is not declared.";
+ parseError(ss.str());
}
else
{
return expr;
}
-Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
+api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
{
bool isBuiltinOperator = false;
// the builtin kind of the overall return expression
- Kind kind = kind::NULL_EXPR;
+ api::Kind kind = api::NULL_EXPR;
// First phase: process the operator
if (Debug.isOn("parser"))
{
- Debug("parser") << "Apply parse op to:" << std::endl;
- Debug("parser") << "args has size " << args.size() << std::endl;
- for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+ Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
+ for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
+ ++i)
{
Debug("parser") << "++ " << *i << std::endl;
}
}
- if (p.d_kind != kind::NULL_EXPR)
+ api::Op op;
+ if (p.d_kind != api::NULL_EXPR)
{
// It is a special case, e.g. tupSel or array constant specification.
// We have to wait until the arguments are parsed to resolve it.
}
else if (!p.d_expr.isNull())
{
- // An explicit operator, e.g. an indexed symbol.
- args.insert(args.begin(), p.d_expr);
- if (p.d_expr.getType().isTester())
+ // An explicit operator, e.g. an apply function
+ api::Kind fkind = getKindForFunction(p.d_expr);
+ if (fkind != api::UNDEFINED_KIND)
{
+ // Some operators may require a specific kind.
// Testers are handled differently than other indexed operators,
// since they require a kind.
- kind = kind::APPLY_TESTER;
+ kind = fkind;
+ Debug("parser") << "Got function kind " << kind << " for expression "
+ << std::endl;
}
+ args.insert(args.begin(), p.d_expr);
+ }
+ else if (!p.d_op.isNull())
+ {
+ // it was given an operator
+ op = p.d_op;
}
else
{
{
// A non-built-in function application, get the expression
checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
- Expr v = getVariable(p.d_name);
+ api::Term v = getVariable(p.d_name);
if (!v.isNull())
{
checkFunctionLike(v);
// Could not find the expression. It may be an overloaded symbol,
// in which case we may find it after knowing the types of its
// arguments.
- std::vector<Type> argTypes;
- for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+ std::vector<api::Sort> argTypes;
+ for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
+ ++i)
{
- argTypes.push_back((*i).getType());
+ argTypes.push_back((*i).getSort());
}
- Expr op = getOverloadedFunctionForTypes(p.d_name, argTypes);
- if (!op.isNull())
+ api::Term fop = getOverloadedFunctionForTypes(p.d_name, argTypes);
+ if (!fop.isNull())
{
- checkFunctionLike(op);
- kind = getKindForFunction(op);
- args.insert(args.begin(), op);
+ checkFunctionLike(fop);
+ kind = getKindForFunction(fop);
+ args.insert(args.begin(), fop);
}
else
{
}
}
}
-
// Second phase: apply the arguments to the parse op
- ExprManager* em = getExprManager();
+ const Options& opts = d_solver->getOptions();
// handle special cases
- if (p.d_kind == kind::STORE_ALL)
+ if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull())
{
if (args.size() != 1)
{
parseError("Too many arguments to array constant.");
}
- if (!args[0].isConst())
+ api::Term constVal = args[0];
+
+ // To parse array constants taking reals whose values are specified by
+ // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
+ // the fact that (/ 1 3) is the division of constants 1 and 3, and not
+ // the resulting constant rational value. Thus, we must construct the
+ // resulting rational here. This also is applied for integral real values
+ // like 5.0 which are converted to (/ 5 1) to distinguish them from
+ // integer constants. We must ensure numerator and denominator are
+ // constant and the denominator is non-zero.
+ if (constVal.getKind() == api::DIVISION)
{
- std::stringstream ss;
- ss << "expected constant term inside array constant, but found "
- << "nonconstant term:" << std::endl
- << "the term: " << args[0];
- parseError(ss.str());
+ std::stringstream sdiv;
+ sdiv << constVal[0] << "/" << constVal[1];
+ constVal = d_solver->mkReal(sdiv.str());
}
- ArrayType aqtype = static_cast<ArrayType>(p.d_type);
- if (!aqtype.getConstituentType().isComparableTo(args[0].getType()))
+
+ if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
{
std::stringstream ss;
ss << "type mismatch inside array constant term:" << std::endl
<< "array type: " << p.d_type << std::endl
- << "expected const type: " << aqtype.getConstituentType() << std::endl
- << "computed const type: " << args[0].getType();
+ << "expected const type: " << p.d_type.getArrayElementSort()
+ << std::endl
+ << "computed const type: " << constVal.getSort();
parseError(ss.str());
}
- return em->mkConst(ArrayStoreAll(p.d_type, args[0]));
+ api::Term ret = d_solver->mkConstArray(p.d_type, constVal);
+ Debug("parser") << "applyParseOp: return store all " << ret << std::endl;
+ return ret;
}
- else if (p.d_kind == kind::APPLY_SELECTOR)
+ else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
{
- if (p.d_expr.isNull())
- {
- parseError("Could not process parsed tuple selector.");
- }
// tuple selector case
- Integer x = p.d_expr.getConst<Rational>().getNumerator();
- if (!x.fitsUnsignedInt())
+ if (!p.d_expr.isUInt64())
{
- parseError("index of tupSel is larger than size of unsigned int");
+ parseError("index of tupSel is larger than size of uint64_t");
}
- unsigned int n = x.toUnsignedInt();
- if (args.size() > 1)
+ uint64_t n = p.d_expr.getUInt64();
+ if (args.size() != 1)
{
- parseError("tupSel applied to more than one tuple argument");
+ parseError("tupSel should only be applied to one tuple argument");
}
- Type t = args[0].getType();
+ api::Sort t = args[0].getSort();
if (!t.isTuple())
{
parseError("tupSel applied to non-tuple");
}
- size_t length = ((DatatypeType)t).getTupleLength();
+ size_t length = t.getTupleLength();
if (n >= length)
{
std::stringstream ss;
ss << "tuple is of length " << length << "; cannot access index " << n;
parseError(ss.str());
}
- const Datatype& dt = ((DatatypeType)t).getDatatype();
- return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args);
+ const api::Datatype& dt = t.getDatatype();
+ api::Term ret = d_solver->mkTerm(
+ api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]);
+ Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
+ return ret;
}
- else if (p.d_kind != kind::NULL_EXPR)
+ else if (p.d_kind == api::TUPLE_PROJECT)
{
- std::stringstream ss;
- ss << "Could not process parsed qualified identifier kind " << p.d_kind;
- parseError(ss.str());
+ api::Term ret = d_solver->mkTerm(p.d_op, args[0]);
+ Debug("parser") << "applyParseOp: return projection " << ret << std::endl;
+ return ret;
+ }
+ else if (p.d_kind != api::NULL_EXPR)
+ {
+ // it should not have an expression or type specified at this point
+ if (!p.d_expr.isNull() || !p.d_type.isNull())
+ {
+ std::stringstream ss;
+ ss << "Could not process parsed qualified identifier kind " << p.d_kind;
+ parseError(ss.str());
+ }
+ // otherwise it is a simple application
+ kind = p.d_kind;
}
else if (isBuiltinOperator)
{
- if (args.size() > 2)
+ if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
{
- if (kind == kind::INTS_DIVISION || kind == kind::XOR
- || kind == kind::MINUS || kind == kind::DIVISION
- || (kind == kind::BITVECTOR_XNOR && v2_6()))
+ // need --uf-ho if these operators are applied over function args
+ for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
+ ++i)
{
- // Builtin operators that are not tokenized, are left associative,
- // but not internally variadic must set this.
- return em->mkLeftAssociative(kind, args);
- }
- else if (kind == kind::IMPLIES)
- {
- /* right-associative, but CVC4 internally only supports 2 args */
- return em->mkRightAssociative(kind, args);
- }
- else if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT
- || kind == kind::LEQ || kind == kind::GEQ)
- {
- /* "chainable", but CVC4 internally only supports 2 args */
- return em->mkExpr(em->mkConst(Chain(kind)), args);
+ if ((*i).getSort().isFunction())
+ {
+ parseError(
+ "Cannot apply equalty to functions unless --uf-ho is set.");
+ }
}
}
-
- if (kind::isAssociative(kind) && args.size() > em->maxArity(kind))
- {
- /* Special treatment for associative operators with lots of children
- */
- return em->mkAssociative(kind, args);
- }
- else if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
- && args.size() == 1)
+ if (!strictModeEnabled() && (kind == api::AND || kind == api::OR)
+ && args.size() == 1)
{
// Unary AND/OR can be replaced with the argument.
+ Debug("parser") << "applyParseOp: return unary " << args[0] << std::endl;
return args[0];
}
- else if (kind == kind::MINUS && args.size() == 1)
+ else if (kind == api::MINUS && args.size() == 1)
{
- return em->mkExpr(kind::UMINUS, args[0]);
+ api::Term ret = d_solver->mkTerm(api::UMINUS, args[0]);
+ Debug("parser") << "applyParseOp: return uminus " << ret << std::endl;
+ return ret;
}
- else
+ if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true")
{
- checkOperator(kind, args.size());
- return em->mkExpr(kind, args);
+ parseError(
+ "eqrange predicate requires option --arrays-exp to be enabled.");
}
+ if (kind == api::SINGLETON && args.size() == 1)
+ {
+ api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]);
+ Debug("parser") << "applyParseOp: return singleton " << ret << std::endl;
+ return ret;
+ }
+ api::Term ret = d_solver->mkTerm(kind, args);
+ Debug("parser") << "applyParseOp: return default builtin " << ret
+ << std::endl;
+ return ret;
}
if (args.size() >= 2)
{
// may be partially applied function, in this case we use HO_APPLY
- Type argt = args[0].getType();
+ api::Sort argt = args[0].getSort();
if (argt.isFunction())
{
- unsigned arity = static_cast<FunctionType>(argt).getArity();
+ unsigned arity = argt.getFunctionArity();
if (args.size() - 1 < arity)
{
+ if (!opts.getUfHo())
+ {
+ parseError("Cannot partially apply functions unless --uf-ho is set.");
+ }
Debug("parser") << "Partial application of " << args[0];
Debug("parser") << " : #argTypes = " << arity;
Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
+ api::Term ret = d_solver->mkTerm(api::HO_APPLY, args);
+ Debug("parser") << "applyParseOp: return curry higher order " << ret
+ << std::endl;
// must curry the partial application
- return em->mkLeftAssociative(kind::HO_APPLY, args);
+ return ret;
}
}
}
- if (kind == kind::NULL_EXPR)
+ if (!op.isNull())
+ {
+ api::Term ret = d_solver->mkTerm(op, args);
+ Debug("parser") << "applyParseOp: return op : " << ret << std::endl;
+ return ret;
+ }
+ if (kind == api::NULL_EXPR)
{
- std::vector<Expr> eargs(args.begin() + 1, args.end());
- return em->mkExpr(args[0], eargs);
+ // should never happen in the new API
+ parseError("do not know how to process parse op");
}
- return em->mkExpr(kind, args);
+ Debug("parser") << "Try default term construction for kind " << kind
+ << " #args = " << args.size() << "..." << std::endl;
+ api::Term ret = d_solver->mkTerm(kind, args);
+ Debug("parser") << "applyParseOp: return : " << ret << std::endl;
+ return ret;
}
-Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
+void Smt2::notifyNamedExpression(api::Term& expr, std::string name)
{
- if (!sexpr.isKeyword())
- {
- parseError("improperly formed :named annotation");
- }
- std::string name = sexpr.getValue();
checkUserSymbol(name);
- // ensure expr is a closed subterm
- if (expr.hasFreeVariable())
- {
- std::stringstream ss;
- ss << ":named annotations can only name terms that are closed";
- parseError(ss.str());
- }
- // check that sexpr is a fresh function symbol, and reserve it
- reserveSymbolAtAssertionLevel(name);
- // define it
- Expr func = mkVar(name, expr.getType(), ExprManager::VAR_FLAG_DEFINED);
- // remember the last term to have been given a :named attribute
+ // remember the expression name in the symbol manager
+ getSymbolManager()->setExpressionName(expr, name, false);
+ // define the variable
+ defineVar(name, expr);
+ // set the last named term, which ensures that we catch when assertions are
+ // named
setLastNamedTerm(expr, name);
- return func;
}
-Expr Smt2::mkAnd(const std::vector<Expr>& es)
+api::Term Smt2::mkAnd(const std::vector<api::Term>& es)
{
- ExprManager* em = getExprManager();
-
if (es.size() == 0)
{
- return em->mkConst(true);
+ return d_solver->mkTrue();
}
else if (es.size() == 1)
{
}
else
{
- return em->mkExpr(kind::AND, es);
+ return d_solver->mkTerm(api::AND, es);
}
}