summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp145
-rw-r--r--src/api/cvc4cpp.h36
-rw-r--r--src/api/cvc4cppkind.h20
-rw-r--r--src/parser/smt2/Smt2.g4
4 files changed, 91 insertions, 114 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 86072d601..4cd9f4923 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -56,8 +56,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
{APPLY, CVC4::Kind::APPLY},
{EQUAL, CVC4::Kind::EQUAL},
{DISTINCT, CVC4::Kind::DISTINCT},
- {VARIABLE, CVC4::Kind::VARIABLE},
- {BOUND_VARIABLE, CVC4::Kind::BOUND_VARIABLE},
+ {CONSTANT, CVC4::Kind::VARIABLE},
+ {VARIABLE, CVC4::Kind::BOUND_VARIABLE},
{LAMBDA, CVC4::Kind::LAMBDA},
{CHOICE, CVC4::Kind::CHOICE},
{CHAIN, CVC4::Kind::CHAIN},
@@ -304,8 +304,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
{CVC4::Kind::APPLY, APPLY},
{CVC4::Kind::EQUAL, EQUAL},
{CVC4::Kind::DISTINCT, DISTINCT},
- {CVC4::Kind::VARIABLE, VARIABLE},
- {CVC4::Kind::BOUND_VARIABLE, BOUND_VARIABLE},
+ {CVC4::Kind::VARIABLE, CONSTANT},
+ {CVC4::Kind::BOUND_VARIABLE, VARIABLE},
{CVC4::Kind::LAMBDA, LAMBDA},
{CVC4::Kind::CHOICE, CHOICE},
{CVC4::Kind::CHAIN, CHAIN},
@@ -1970,7 +1970,7 @@ Term Solver::mkPi() const
}
template <typename T>
-Term Solver::mkConstHelper(T t) const
+Term Solver::mkValHelper(T t) const
{
try
{
@@ -1997,7 +1997,7 @@ Term Solver::mkRealFromStrHelper(std::string s) const
CVC4::Rational r = s.find('/') != std::string::npos
? CVC4::Rational(s)
: CVC4::Rational::fromDecimal(s);
- return mkConstHelper<CVC4::Rational>(r);
+ return mkValHelper<CVC4::Rational>(r);
}
catch (const std::invalid_argument& e)
{
@@ -2020,7 +2020,7 @@ Term Solver::mkReal(int32_t val) const
{
try
{
- return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+ return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
}
catch (const std::invalid_argument& e)
{
@@ -2032,7 +2032,7 @@ Term Solver::mkReal(int64_t val) const
{
try
{
- return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+ return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
}
catch (const std::invalid_argument& e)
{
@@ -2044,7 +2044,7 @@ Term Solver::mkReal(uint32_t val) const
{
try
{
- return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+ return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
}
catch (const std::invalid_argument& e)
{
@@ -2056,7 +2056,7 @@ Term Solver::mkReal(uint64_t val) const
{
try
{
- return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+ return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
}
catch (const std::invalid_argument& e)
{
@@ -2068,7 +2068,7 @@ Term Solver::mkReal(int32_t num, int32_t den) const
{
try
{
- return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+ return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
}
catch (const std::invalid_argument& e)
{
@@ -2080,7 +2080,7 @@ Term Solver::mkReal(int64_t num, int64_t den) const
{
try
{
- return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+ return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
}
catch (const std::invalid_argument& e)
{
@@ -2092,7 +2092,7 @@ Term Solver::mkReal(uint32_t num, uint32_t den) const
{
try
{
- return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+ return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
}
catch (const std::invalid_argument& e)
{
@@ -2104,7 +2104,7 @@ Term Solver::mkReal(uint64_t num, uint64_t den) const
{
try
{
- return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+ return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
}
catch (const std::invalid_argument& e)
{
@@ -2146,7 +2146,7 @@ Term Solver::mkEmptySet(Sort s) const
{
CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
<< "null sort or set sort";
- return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
+ return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
}
Term Solver::mkSepNil(Sort sort) const
@@ -2166,22 +2166,22 @@ Term Solver::mkSepNil(Sort sort) const
Term Solver::mkString(const char* s, bool useEscSequences) const
{
- return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
+ return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
}
Term Solver::mkString(const std::string& s, bool useEscSequences) const
{
- return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
+ return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
}
Term Solver::mkString(const unsigned char c) const
{
- return mkConstHelper<CVC4::String>(CVC4::String(std::string(1, c)));
+ return mkValHelper<CVC4::String>(CVC4::String(std::string(1, c)));
}
Term Solver::mkString(const std::vector<unsigned>& s) const
{
- return mkConstHelper<CVC4::String>(CVC4::String(s));
+ return mkValHelper<CVC4::String>(CVC4::String(s));
}
Term Solver::mkUniverseSet(Sort sort) const
@@ -2207,7 +2207,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
try
{
- return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+ return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
}
catch (const std::invalid_argument& e)
{
@@ -2228,7 +2228,7 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
<< "base 2, 10, or 16";
try
{
- return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
+ return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
}
catch (const std::invalid_argument& e)
{
@@ -2249,7 +2249,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
CVC4_API_CHECK(val.modByPow2(size) == val)
<< "Overflow in bitvector construction (specified bitvector size "
<< size << " too small to hold value " << s << ")";
- return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+ return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
}
catch (const std::invalid_argument& e)
{
@@ -2283,7 +2283,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
{
CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
<< "Expected CVC4 to be compiled with SymFPU support";
- return mkConstHelper<CVC4::FloatingPoint>(
+ return mkValHelper<CVC4::FloatingPoint>(
FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
}
@@ -2291,7 +2291,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
{
CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
<< "Expected CVC4 to be compiled with SymFPU support";
- return mkConstHelper<CVC4::FloatingPoint>(
+ return mkValHelper<CVC4::FloatingPoint>(
FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
}
@@ -2299,7 +2299,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
{
CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
<< "Expected CVC4 to be compiled with SymFPU support";
- return mkConstHelper<CVC4::FloatingPoint>(
+ return mkValHelper<CVC4::FloatingPoint>(
FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
}
@@ -2307,7 +2307,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
{
CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
<< "Expected CVC4 to be compiled with SymFPU support";
- return mkConstHelper<CVC4::FloatingPoint>(
+ return mkValHelper<CVC4::FloatingPoint>(
FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
}
@@ -2315,19 +2315,19 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
{
CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
<< "Expected CVC4 to be compiled with SymFPU support";
- return mkConstHelper<CVC4::FloatingPoint>(
+ return mkValHelper<CVC4::FloatingPoint>(
FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
}
Term Solver::mkRoundingMode(RoundingMode rm) const
{
- return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
+ return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
}
Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
{
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- return mkConstHelper<CVC4::UninterpretedConstant>(
+ return mkValHelper<CVC4::UninterpretedConstant>(
CVC4::UninterpretedConstant(*sort.d_type, index));
}
@@ -2385,14 +2385,14 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
CVC4_API_ARG_CHECK_EXPECTED(
val.getSort().isBitVector() && val.d_expr->isConst(), val)
<< "bit-vector constant";
- return mkConstHelper<CVC4::FloatingPoint>(
+ return mkValHelper<CVC4::FloatingPoint>(
CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
}
-/* Create variables */
+/* Create constants */
/* -------------------------------------------------------------------------- */
-Term Solver::mkVar(Sort sort, const std::string& symbol) const
+Term Solver::mkConst(Sort sort, const std::string& symbol) const
{
try
{
@@ -2408,7 +2408,10 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
}
}
-Term Solver::mkBoundVar(Sort sort, const std::string& symbol) const
+/* Create variables */
+/* -------------------------------------------------------------------------- */
+
+Term Solver::mkVar(Sort sort, const std::string& symbol) const
{
try
{
@@ -2436,8 +2439,9 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
kind)
<< "Only operator-style terms are created with mkTerm(), "
- "to create variables and constants see mkVar(), mkBoundVar(), "
- "and mkConst().";
+ "to create variables, constants and values see mkVar(), mkConst() "
+ "and the respective theory-specific functions to create values, "
+ "e.g., mkBitVector().";
CVC4_API_KIND_CHECK_EXPECTED(
nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
<< "Terms with kind " << kindToString(kind) << " must have at least "
@@ -2729,15 +2733,14 @@ std::vector<Expr> Solver::termVectorToExprs(
OpTerm Solver::mkOpTerm(Kind kind, Kind k)
{
CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
- return *mkConstHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
+ return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
}
OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg)
{
CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind)
<< "RECORD_UPDATE_OP";
- return *mkConstHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg))
- .d_expr.get();
+ return *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get();
}
OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
@@ -2747,59 +2750,59 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
switch (kind)
{
case DIVISIBLE_OP:
- res = *mkConstHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
+ res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
break;
case BITVECTOR_REPEAT_OP:
- res = *mkConstHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+ res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
.d_expr.get();
break;
case BITVECTOR_ZERO_EXTEND_OP:
- res = *mkConstHelper<CVC4::BitVectorZeroExtend>(
+ res = *mkValHelper<CVC4::BitVectorZeroExtend>(
CVC4::BitVectorZeroExtend(arg))
.d_expr.get();
break;
case BITVECTOR_SIGN_EXTEND_OP:
- res = *mkConstHelper<CVC4::BitVectorSignExtend>(
+ res = *mkValHelper<CVC4::BitVectorSignExtend>(
CVC4::BitVectorSignExtend(arg))
.d_expr.get();
break;
case BITVECTOR_ROTATE_LEFT_OP:
- res = *mkConstHelper<CVC4::BitVectorRotateLeft>(
+ res = *mkValHelper<CVC4::BitVectorRotateLeft>(
CVC4::BitVectorRotateLeft(arg))
.d_expr.get();
break;
case BITVECTOR_ROTATE_RIGHT_OP:
- res = *mkConstHelper<CVC4::BitVectorRotateRight>(
+ res = *mkValHelper<CVC4::BitVectorRotateRight>(
CVC4::BitVectorRotateRight(arg))
.d_expr.get();
break;
case INT_TO_BITVECTOR_OP:
- res = *mkConstHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
+ res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
.d_expr.get();
break;
case FLOATINGPOINT_TO_UBV_OP:
- res = *mkConstHelper<CVC4::FloatingPointToUBV>(
- CVC4::FloatingPointToUBV(arg))
- .d_expr.get();
+ res =
+ *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_UBV_TOTAL_OP:
- res = *mkConstHelper<CVC4::FloatingPointToUBVTotal>(
+ res = *mkValHelper<CVC4::FloatingPointToUBVTotal>(
CVC4::FloatingPointToUBVTotal(arg))
.d_expr.get();
break;
case FLOATINGPOINT_TO_SBV_OP:
- res = *mkConstHelper<CVC4::FloatingPointToSBV>(
- CVC4::FloatingPointToSBV(arg))
- .d_expr.get();
+ res =
+ *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_SBV_TOTAL_OP:
- res = *mkConstHelper<CVC4::FloatingPointToSBVTotal>(
+ res = *mkValHelper<CVC4::FloatingPointToSBVTotal>(
CVC4::FloatingPointToSBVTotal(arg))
.d_expr.get();
break;
case TUPLE_UPDATE_OP:
- res = *mkConstHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg))
- .d_expr.get();
+ res =
+ *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get();
break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
@@ -2816,37 +2819,37 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
switch (kind)
{
case BITVECTOR_EXTRACT_OP:
- res = *mkConstHelper<CVC4::BitVectorExtract>(
+ res = *mkValHelper<CVC4::BitVectorExtract>(
CVC4::BitVectorExtract(arg1, arg2))
.d_expr.get();
break;
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
- res = *mkConstHelper<CVC4::FloatingPointToFPIEEEBitVector>(
+ res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
.d_expr.get();
break;
case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
- res = *mkConstHelper<CVC4::FloatingPointToFPFloatingPoint>(
+ res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
.d_expr.get();
break;
case FLOATINGPOINT_TO_FP_REAL_OP:
- res = *mkConstHelper<CVC4::FloatingPointToFPReal>(
+ res = *mkValHelper<CVC4::FloatingPointToFPReal>(
CVC4::FloatingPointToFPReal(arg1, arg2))
.d_expr.get();
break;
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
- res = *mkConstHelper<CVC4::FloatingPointToFPSignedBitVector>(
+ res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
.d_expr.get();
break;
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
- res = *mkConstHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
+ res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
.d_expr.get();
break;
case FLOATINGPOINT_TO_FP_GENERIC_OP:
- res = *mkConstHelper<CVC4::FloatingPointToFPGeneric>(
+ res = *mkValHelper<CVC4::FloatingPointToFPGeneric>(
CVC4::FloatingPointToFPGeneric(arg1, arg2))
.d_expr.get();
break;
@@ -2940,24 +2943,6 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
}
/**
- * ( declare-const <symbol> <sort> )
- */
-Term Solver::declareConst(const std::string& symbol, Sort sort) const
-{
- try
- {
- CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res = d_exprMgr->mkVar(symbol, *sort.d_type);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
- }
- catch (const CVC4::TypeCheckingException& e)
- {
- throw CVC4ApiException(e.getMessage());
- }
-}
-
-/**
* ( declare-datatype <symbol> <datatype_decl> )
*/
Sort Solver::declareDatatype(
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 203586066..c13c7919e 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2166,20 +2166,23 @@ class CVC4_PUBLIC Solver
/* .................................................................... */
/**
- * Create variable.
- * @param sort the sort of the variable
- * @param symbol the name of the variable
- * @return the variable
+ * Create (first-order) constant (0-arity function symbol).
+ * SMT-LIB: ( declare-const <symbol> <sort> )
+ * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
+ *
+ * @param sort the sort of the constant
+ * @param symbol the name of the constant
+ * @return the first-order constant
*/
- Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
+ Term mkConst(Sort sort, const std::string& symbol = std::string()) const;
/**
- * Create bound variable.
+ * Create (bound) variable.
* @param sort the sort of the variable
* @param symbol the name of the variable
* @return the variable
*/
- Term mkBoundVar(Sort sort, const std::string& symbol = std::string()) const;
+ Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
/* .................................................................... */
/* Formula Handling */
@@ -2246,17 +2249,6 @@ class CVC4_PUBLIC Solver
Result checkValidAssuming(const std::vector<Term>& assumptions) const;
/**
- * Declare first-order constant (0-arity function symbol).
- * SMT-LIB: ( declare-const <symbol> <sort> )
- * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
- * This command corresponds to mkVar().
- * @param symbol the name of the first-order constant
- * @param sort the sort of the first-order constant
- * @return the first-order constant
- */
- Term declareConst(const std::string& symbol, Sort sort) const;
-
- /**
* Create datatype sort.
* SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
* @param symbol the name of the datatype sort
@@ -2303,7 +2295,7 @@ class CVC4_PUBLIC Solver
/**
* Define n-ary function.
* SMT-LIB: ( define-fun <function_def> )
- * Create parameter 'fun' with mkVar().
+ * Create parameter 'fun' with mkConst().
* @param fun the sorted function
* @param bound_vars the parameters to this function
* @param term the function body
@@ -2330,7 +2322,7 @@ class CVC4_PUBLIC Solver
/**
* Define recursive function.
* SMT-LIB: ( define-fun-rec <function_def> )
- * Create parameter 'fun' with mkVar().
+ * Create parameter 'fun' with mkConst().
* @param fun the sorted function
* @param bound_vars the parameters to this function
* @param term the function body
@@ -2343,7 +2335,7 @@ class CVC4_PUBLIC Solver
/**
* Define recursive functions.
* SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
- * Create elements of parameter 'funs' with mkVar().
+ * Create elements of parameter 'funs' with mkConst().
* @param funs the sorted functions
* @param bound_vars the list of parameters to the functions
* @param term the list of function bodies of the functions
@@ -2506,7 +2498,7 @@ class CVC4_PUBLIC Solver
void checkMkTerm(Kind kind, uint32_t nchildren) const;
/* Helper for mk-functions that call d_exprMgr->mkConst(). */
template <typename T>
- Term mkConstHelper(T t) const;
+ Term mkValHelper(T t) const;
/* Helper for mkReal functions that take a string as argument. */
Term mkRealFromStrHelper(std::string s) const;
/* Helper for mkBitVector functions that take a string as argument. */
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 3aba6cebb..d4f6880f9 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -123,25 +123,25 @@ enum CVC4_PUBLIC Kind : int32_t
*/
DISTINCT,
/**
- * Variable.
+ * First-order constant.
* Not permitted in bindings (forall, exists, ...).
* Parameters:
- * See mkVar().
+ * See mkConst().
* Create with:
- * mkVar(const std::string& symbol, Sort sort)
- * mkVar(Sort sort)
+ * mkConst(const std::string& symbol, Sort sort)
+ * mkConst(Sort sort)
*/
- VARIABLE,
+ CONSTANT,
/**
- * Bound variable.
+ * (Bound) variable.
* Permitted in bindings and in the lambda and quantifier bodies only.
* Parameters:
- * See mkBoundVar().
+ * See mkVar().
* Create with:
- * mkBoundVar(const std::string& symbol, Sort sort)
- * mkBoundVar(Sort sort)
+ * mkVar(const std::string& symbol, Sort sort)
+ * mkVar(Sort sort)
*/
- BOUND_VARIABLE,
+ VARIABLE,
#if 0
/* Skolem variable (internal only) */
SKOLEM,
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 00f2e944d..75df38637 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2307,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm]
sortSymbol[type,CHECK_DECLARED]
sortSymbol[type2,CHECK_DECLARED]
{
- api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1");
- api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2");
+ api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
+ api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback