#include "expr/node_manager_attributes.h"
#include "expr/sequence.h"
#include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
#include "options/base_options.h"
#include "options/main_options.h"
#include "options/option_exception.h"
#include "theory/datatypes/tuple_project_op.h"
#include "theory/logic_info.h"
#include "theory/theory_model.h"
-#include "util/abstract_value.h"
#include "util/bitvector.h"
#include "util/divisible.h"
#include "util/floatingpoint.h"
#include "util/statistics_stats.h"
#include "util/statistics_value.h"
#include "util/string.h"
+#include "util/uninterpreted_sort_value.h"
#include "util/utility.h"
namespace cvc5 {
{UNDEFINED_KIND, cvc5::Kind::UNDEFINED_KIND},
{NULL_EXPR, cvc5::Kind::NULL_EXPR},
/* Builtin ------------------------------------------------------------- */
- {UNINTERPRETED_CONSTANT, cvc5::Kind::UNINTERPRETED_CONSTANT},
- {ABSTRACT_VALUE, cvc5::Kind::ABSTRACT_VALUE},
+ {UNINTERPRETED_SORT_VALUE, cvc5::Kind::UNINTERPRETED_SORT_VALUE},
{EQUAL, cvc5::Kind::EQUAL},
{DISTINCT, cvc5::Kind::DISTINCT},
{CONSTANT, cvc5::Kind::VARIABLE},
{cvc5::Kind::UNDEFINED_KIND, UNDEFINED_KIND},
{cvc5::Kind::NULL_EXPR, NULL_EXPR},
/* Builtin --------------------------------------------------------- */
- {cvc5::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT},
- {cvc5::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE},
+ {cvc5::Kind::UNINTERPRETED_SORT_VALUE, UNINTERPRETED_SORT_VALUE},
{cvc5::Kind::EQUAL, EQUAL},
{cvc5::Kind::DISTINCT, DISTINCT},
{cvc5::Kind::VARIABLE, CONSTANT},
CVC5_API_TRY_CATCH_END;
}
-bool Term::isAbstractValue() const
+bool Term::isUninterpretedSortValue() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
//////// all checks before this line
- return d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE;
+ return d_node->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE;
////////
CVC5_API_TRY_CATCH_END;
}
-std::string Term::getAbstractValue() const
+std::string Term::getUninterpretedSortValue() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
- CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE,
- *d_node)
+ CVC5_API_ARG_CHECK_EXPECTED(
+ d_node->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE, *d_node)
<< "Term to be an abstract value when calling "
- "getAbstractValue()";
+ "getUninterpretedSortValue()";
//////// all checks before this line
- return d_node->getConst<AbstractValue>().getIndex().toString();
+ std::stringstream ss;
+ ss << d_node->getConst<UninterpretedSortValue>();
+ return ss.str();
////////
CVC5_API_TRY_CATCH_END;
}
CVC5_API_TRY_CATCH_END;
}
-bool Term::isUninterpretedValue() const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK_NOT_NULL;
- //////// all checks before this line
- return d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT;
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-std::pair<Sort, std::int32_t> Term::getUninterpretedValue() const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK_NOT_NULL;
- CVC5_API_ARG_CHECK_EXPECTED(
- d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT, *d_node)
- << "Term to be an uninterpreted value when calling "
- "getUninterpretedValue()";
- //////// all checks before this line
- const auto& uc = d_node->getConst<UninterpretedConstant>();
- return std::make_pair(Sort(d_solver, uc.getType()),
- uc.getIndex().toUnsignedInt());
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
std::ostream& operator<<(std::ostream& out, const Term& t)
{
out << t.toString();
CVC5_API_TRY_CATCH_END;
}
-Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_SOLVER_CHECK_SORT(sort);
- //////// all checks before this line
- return mkValHelper<cvc5::UninterpretedConstant>(
- cvc5::UninterpretedConstant(*sort.d_type, index));
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
-Term Solver::mkAbstractValue(const std::string& index) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string";
-
- cvc5::Integer idx(index, 10);
- CVC5_API_ARG_CHECK_EXPECTED(idx > 0, index)
- << "a string representing an integer > 0";
- //////// all checks before this line
- return Term(this, getNodeManager()->mkConst(cvc5::AbstractValue(idx)));
- // do not call getType(), for abstract values, type can not be computed
- // until it is substituted away
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
-Term Solver::mkAbstractValue(uint64_t index) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
- //////// all checks before this line
- return Term(this,
- getNodeManager()->mkConst(cvc5::AbstractValue(Integer(index))));
- // do not call getType(), for abstract values, type can not be computed
- // until it is substituted away
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
{
CVC5_API_TRY_CATCH_BEGIN;
/**
* @return true if the term is an abstract value.
*/
- bool isAbstractValue() const;
+ bool isUninterpretedSortValue() const;
/**
- * Asserts isAbstractValue().
- * @return the representation of an abstract value as a string.
+ * Asserts isUninterpretedSortValue().
+ * @return the representation of an uninterpreted sort value as a string.
*/
- std::string getAbstractValue() const;
+ std::string getUninterpretedSortValue() const;
/**
* @return true if the term is a tuple value.
*/
std::vector<Term> getSequenceValue() const;
- /**
- * @return true if the term is a value from an uninterpreted sort.
- */
- bool isUninterpretedValue() const;
- /**
- bool @return() const;
- * Asserts isUninterpretedValue().
- * @return the representation of an uninterpreted value as a pair of its
- sort and its
- * index.
- */
- std::pair<Sort, int32_t> getUninterpretedValue() const;
-
protected:
/**
* The associated solver object.
*/
Term mkRoundingMode(RoundingMode rm) const;
- /**
- * Create uninterpreted constant.
- * @param sort Sort of the constant
- * @param index Index of the constant
- */
- Term mkUninterpretedConst(const Sort& sort, int32_t index) const;
-
- /**
- * Create an abstract value constant.
- * The given index needs to be a positive integer in base 10.
- * @param index Index of the abstract value
- */
- Term mkAbstractValue(const std::string& index) const;
-
- /**
- * Create an abstract value constant.
- * The given index needs to be positive.
- * @param index Index of the abstract value
- */
- Term mkAbstractValue(uint64_t index) const;
-
/**
* Create a floating-point constant.
* @param exp Size of the exponent
/* Builtin --------------------------------------------------------------- */
/**
- * Uninterpreted constant.
- *
- * Parameters:
- * - 1: Sort of the constant
- * - 2: Index of the constant
- *
- * Create with:
- * - `Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const`
- */
- UNINTERPRETED_CONSTANT,
- /**
- * Abstract value (other than uninterpreted sort constants).
+ * Abstract value.
*
* Parameters:
* - 1: Index of the abstract value
*
* Create with:
- * - `Solver::mkAbstractValue(const std::string& index) const`
- * - `Solver::mkAbstractValue(uint64_t index) const`
+ * - `Solver::mkUninterpretedSortValue(const std::string& index) const`
+ * - `Solver::mkUninterpretedSortValue(uint64_t index) const`
*/
- ABSTRACT_VALUE,
+ UNINTERPRETED_SORT_VALUE,
#if 0
/* Built-in operator */
BUILTIN,
private native long mkRoundingMode(long pointer, int rm);
- /**
- * Create uninterpreted constant.
- * @param sort Sort of the constant
- * @param index Index of the constant
- */
- public Term mkUninterpretedConst(Sort sort, int index) throws CVC5ApiException
- {
- Utils.validateUnsigned(index, "index");
- long termPointer = mkUninterpretedConst(pointer, sort.getPointer(), index);
- return new Term(this, termPointer);
- }
-
- private native long mkUninterpretedConst(long pointer, long sortPointer, int index);
-
- /**
- * Create an abstract value constant.
- * @param index Index of the abstract value
- */
- public Term mkAbstractValue(String index)
- {
- long termPointer = mkAbstractValue(pointer, index);
- return new Term(this, termPointer);
- }
-
- private native long mkAbstractValue(long pointer, String index);
-
- /**
- * Create an abstract value constant.
- * @param index Index of the abstract value
- */
- public Term mkAbstractValue(long index) throws CVC5ApiException
- {
- Utils.validateUnsigned(index, "index");
- long termPointer = mkAbstractValue(pointer, index);
- return new Term(this, termPointer);
- }
-
- private native long mkAbstractValue(long pointer, long index);
-
/**
* Create a floating-point constant.
* @param exp Size of the exponent
private native String getBitVectorValue(long pointer, int base);
/**
- * @return true if the term is an abstract value.
+ * @return true if the term is an uninterpreted sort value.
*/
- public boolean isAbstractValue()
+ public boolean isUninterpretedSortValue()
{
- return isAbstractValue(pointer);
+ return isUninterpretedSortValue(pointer);
}
- private native boolean isAbstractValue(long pointer);
+ private native boolean isUninterpretedSortValue(long pointer);
/**
- * Asserts isAbstractValue().
- * @return the representation of an abstract value as a string.
+ * Asserts isUninterpretedSortValue().
+ * @return the representation of an uninterpreted sort value as a string.
*/
- public String getAbstractValue()
+ public String getUninterpretedSortValue()
{
- return getAbstractValue(pointer);
+ return getUninterpretedSortValue(pointer);
}
- private native String getAbstractValue(long pointer);
+ private native String getUninterpretedSortValue(long pointer);
/**
* @return true if the term is a tuple value.
private native long[] getSequenceValue(long pointer);
- /**
- * @return true if the term is a value from an uninterpreted sort.
- */
- public boolean isUninterpretedValue()
- {
- return isUninterpretedValue(pointer);
- }
-
- private native boolean isUninterpretedValue(long pointer);
-
- /**
- boolean @return()
- * Asserts isUninterpretedValue().
- * @return the representation of an uninterpreted value as a pair of its
- sort and its
- * index.
- */
- public Pair<Sort, Integer> getUninterpretedValue()
- {
- Pair<Long, Integer> pair = getUninterpretedValue(pointer);
- Sort sort = new Sort(solver, pair.first);
- return new Pair<Sort, Integer>(sort, pair.second);
- }
-
- private native Pair<Long, Integer> getUninterpretedValue(long pointer);
-
public class ConstIterator implements Iterator<Term>
{
private int currentIndex;
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
-/*
- * Class: io_github_cvc5_api_Solver
- * Method: mkUninterpretedConst
- * Signature: (JJI)J
- */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUninterpretedConst(
- JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint index)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Solver* solver = reinterpret_cast<Solver*>(pointer);
- Sort* sort = reinterpret_cast<Sort*>(sortPointer);
- Term* retPointer =
- new Term(solver->mkUninterpretedConst(*sort, (int32_t)index));
- return reinterpret_cast<jlong>(retPointer);
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
-/*
- * Class: io_github_cvc5_api_Solver
- * Method: mkAbstractValue
- * Signature: (JLjava/lang/String;)J
- */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_api_Solver_mkAbstractValue__JLjava_lang_String_2(
- JNIEnv* env, jobject, jlong pointer, jstring jIndex)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Solver* solver = reinterpret_cast<Solver*>(pointer);
- const char* s = env->GetStringUTFChars(jIndex, nullptr);
- std::string cIndex(s);
- Term* retPointer = new Term(solver->mkAbstractValue(cIndex));
- env->ReleaseStringUTFChars(jIndex, s);
- return reinterpret_cast<jlong>(retPointer);
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
-/*
- * Class: io_github_cvc5_api_Solver
- * Method: mkAbstractValue
- * Signature: (JJ)J
- */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkAbstractValue__JJ(
- JNIEnv* env, jobject, jlong pointer, jlong index)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Solver* solver = reinterpret_cast<Solver*>(pointer);
- Term* retPointer = new Term(solver->mkAbstractValue((uint64_t)index));
- return reinterpret_cast<jlong>(retPointer);
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
/*
* Class: io_github_cvc5_api_Solver
* Method: mkFloatingPoint
}
/*
+ * Class: cvc5_Term
* Class: io_github_cvc5_api_Term
- * Method: isAbstractValue
+ * Method: isUninterpretedSortValue
* Signature: (J)Z
*/
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isAbstractValue(
- JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jboolean JNICALL
+Java_io_github_cvc5_api_Term_isUninterpretedSortValue(JNIEnv* env,
+ jobject,
+ jlong pointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Term* current = reinterpret_cast<Term*>(pointer);
- return static_cast<jboolean>(current->isAbstractValue());
+ return static_cast<jboolean>(current->isUninterpretedSortValue());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
}
/*
* Class: io_github_cvc5_api_Term
- * Method: getAbstractValue
+ * Method: getUninterpretedSortValue
* Signature: (J)Ljava/lang/String;
*/
-JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getAbstractValue(
- JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jstring JNICALL
+Java_io_github_cvc5_api_Term_getUninterpretedSortValue(JNIEnv* env,
+ jobject,
+ jlong pointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Term* current = reinterpret_cast<Term*>(pointer);
- std::string ret = current->getAbstractValue();
+ std::string ret = current->getUninterpretedSortValue();
return env->NewStringUTF(ret.c_str());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
}
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
}
-/*
- * Class: io_github_cvc5_api_Term
- * Method: isUninterpretedValue
- * Signature: (J)Z
- */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isUninterpretedValue(
- JNIEnv* env, jobject, jlong pointer)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Term* current = reinterpret_cast<Term*>(pointer);
- return static_cast<jboolean>(current->isUninterpretedValue());
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
-}
-
-/*
- * Class: io_github_cvc5_api_Term
- * Method: getUninterpretedValue
- * Signature: (J)Lio/github/cvc5/api/Pair;
- */
-JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getUninterpretedValue(
- JNIEnv* env, jobject, jlong pointer)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Term* current = reinterpret_cast<Term*>(pointer);
- std::pair<Sort, std::int32_t> value = current->getUninterpretedValue();
-
- Sort* sort = new Sort(value.first);
- jlong sortPointer = reinterpret_cast<jlong>(sort);
-
- // Long longObject = new Long(pointer)
- jclass longClass = env->FindClass("Ljava/lang/Long;");
- jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
- jobject longObject = env->NewObject(longClass, longConstructor, sortPointer);
-
- // Integer integerObject = new Integer(pair.second)
- jclass integerClass = env->FindClass("Ljava/lang/Integer;");
- jmethodID integerConstructor =
- env->GetMethodID(integerClass, "<init>", "(I)V");
- jobject integerObject = env->NewObject(
- integerClass, integerConstructor, static_cast<jint>(value.second));
-
- // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject)
- jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;");
- jmethodID pairConstructor = env->GetMethodID(
- pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V");
- jobject pair =
- env->NewObject(pairClass, pairConstructor, longObject, integerObject);
-
- return pair;
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
/*
* Class: io_github_cvc5_api_Term
* Method: iterator
Term mkPosZero(uint32_t exp, uint32_t sig) except +
Term mkNegZero(uint32_t exp, uint32_t sig) except +
Term mkRoundingMode(RoundingMode rm) except +
- Term mkUninterpretedConst(Sort sort, int32_t index) except +
Term mkAbstractValue(const string& index) except +
Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except +
Term mkCardinalityConstraint(Sort sort, int32_t index) except +
string getRealValue() except +
bint isBitVectorValue() except +
string getBitVectorValue(uint32_t base) except +
- bint isAbstractValue() except +
- string getAbstractValue() except +
+ bint isUninterpretedSortValue() except +
+ string getUninterpretedSortValue() except +
bint isFloatingPointPosZero() except +
bint isFloatingPointNegZero() except +
bint isFloatingPointPosInf() except +
set[Term] getSetValue() except +
bint isSequenceValue() except +
vector[Term] getSequenceValue() except +
- bint isUninterpretedValue() except +
- pair[Sort, int32_t] getUninterpretedValue() except +
bint isTupleValue() except +
vector[Term] getTupleValue() except +
term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
return term
- def mkUninterpretedConst(self, Sort sort, int index):
- """Create uninterpreted constant.
-
- :param sort: Sort of the constant
- :param index: Index of the constant
- """
- cdef Term term = Term(self)
- term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index)
- return term
-
- def mkAbstractValue(self, index):
- """
- Create an abstract value constant.
- The given index needs to be positive.
-
- :param index: Index of the abstract value
- """
- cdef Term term = Term(self)
- try:
- term.cterm = self.csolver.mkAbstractValue(str(index).encode())
- except:
- raise ValueError(
- "mkAbstractValue expects a str representing a number"
- " or an int, but got{}".format(index))
- return term
-
def mkFloatingPoint(self, int exp, int sig, Term val):
"""Create a floating-point constant.
"""
return int(self.cterm.getIntegerValue().decode())
- def isAbstractValue(self):
- """:return: True iff this term is an abstract value."""
- return self.cterm.isAbstractValue()
-
- def getAbstractValue(self):
- """
- Asserts :py:meth:`isAbstractValue()`.
-
- :return: the representation of an abstract value as a string.
- """
- return self.cterm.getAbstractValue().decode()
-
def isFloatingPointPosZero(self):
""":return: True iff the term is the floating-point value for positive zero."""
return self.cterm.isFloatingPointPosZero()
elems.append(term)
return elems
- def isUninterpretedValue(self):
+ def isUninterpretedSortValue(self):
""":return: True iff this term is a value from an uninterpreted sort."""
- return self.cterm.isUninterpretedValue()
+ return self.cterm.isUninterpretedSortValue()
- def getUninterpretedValue(self):
+ def getUninterpretedSortValue(self):
"""
- Asserts :py:meth:`isUninterpretedValue()`.
+ Asserts :py:meth:`isUninterpretedSortValue()`.
:return: the representation of an uninterpreted value as a pair of its sort and its index.
"""
- cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue()
- cdef Sort sort = Sort(self.solver)
- sort.csort = p.first
- i = p.second
- return (sort, i)
+ return self.cterm.getUninterpretedSortValue()
def isTupleValue(self):
""":return: True iff this term is a tuple value."""
subs.h
sygus_datatype.cpp
sygus_datatype.h
- uninterpreted_constant.cpp
- uninterpreted_constant.h
variadic_trie.cpp
variadic_trie.h
)
#include "expr/type_properties.h"
#include "theory/bags/bag_make_op.h"
#include "theory/sets/singleton_op.h"
-#include "theory/type_enumerator.h"
-#include "util/abstract_value.h"
#include "util/bitvector.h"
#include "util/poly_util.h"
#include "util/rational.h"
#include "util/resource_manager.h"
+#include "util/uninterpreted_sort_value.h"
// clang-format off
${metakind_includes}
return bag;
}
-Node NodeManager::mkAbstractValue(const TypeNode& type)
+Node NodeManager::mkUninterpretedSortValue(const TypeNode& type)
{
- Node n = mkConst(AbstractValue(++d_abstractValueCount));
- n.setAttribute(TypeAttr(), type);
- n.setAttribute(TypeCheckedAttr(), true);
+ Node n = mkConst(UninterpretedSortValue(type, ++d_abstractValueCount));
return n;
}
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
- /** Make a new abstract value with the given type. */
- Node mkAbstractValue(const TypeNode& type);
+ /** Make a new uninterpreted sort value with the given type. */
+ Node mkUninterpretedSortValue(const TypeNode& type);
/** make unique (per Type,Kind) variable. */
Node mkNullaryOperator(const TypeNode& type, Kind k);
};
typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
+struct AbstractValueId
+{
+};
+using AbstractValueAttribute = expr::Attribute<AbstractValueId, bool>;
+
const char* toString(SkolemFunId id)
{
switch (id)
return nullptr;
}
+bool SkolemManager::isAbstractValue(TNode n) const
+{
+ AbstractValueAttribute ava;
+ return n.getAttribute(ava);
+}
+
Node SkolemManager::getWitnessForm(Node k)
{
Assert(k.getKind() == SKOLEM);
}
n.setAttribute(expr::TypeAttr(), type);
n.setAttribute(expr::TypeCheckedAttr(), true);
+
+ if ((flags & SKOLEM_ABSTRACT_VALUE) != 0)
+ {
+ AbstractValueAttribute ava;
+ n.setAttribute(ava, true);
+ }
+
return n;
}
*/
enum SkolemFlags
{
- SKOLEM_DEFAULT = 0, /**< default behavior */
- SKOLEM_EXACT_NAME = 1, /**< do not make the name unique by adding the id */
- SKOLEM_BOOL_TERM_VAR = 2 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
+ /** default behavior */
+ SKOLEM_DEFAULT = 0,
+ /** do not make the name unique by adding the id */
+ SKOLEM_EXACT_NAME = 1,
+ /** vars requiring kind BOOLEAN_TERM_VARIABLE */
+ SKOLEM_BOOL_TERM_VAR = 2,
+ /** a skolem that stands for an abstract value (used for printing) */
+ SKOLEM_ABSTRACT_VALUE = 4,
};
/**
* This makes a skolem of same type as bound variable v, (say its type is T),
* the proof generator that was provided in a call to mkSkolem above.
*/
ProofGenerator* getProofGenerator(Node q) const;
+
+ /** Returns true if n is a skolem that stands for an abstract value */
+ bool isAbstractValue(TNode n) const;
+
/**
* Convert to witness form, which gets the witness form of a skolem k.
* Notice this method is *not* recursive, instead, it is a simple attribute
* by this node manager.
*/
size_t d_skolemCounter;
+
/** Get or make skolem attribute for term w, which may be a witness term */
Node mkSkolemInternal(Node w,
const std::string& prefix,
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andres Noetzli, Andrew Reynolds, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Representation of constants of uninterpreted sorts.
- */
-
-#include "expr/uninterpreted_constant.h"
-
-#include <algorithm>
-#include <iostream>
-#include <sstream>
-#include <string>
-
-#include "base/check.h"
-#include "expr/type_node.h"
-
-using namespace std;
-
-namespace cvc5 {
-
-UninterpretedConstant::UninterpretedConstant(const TypeNode& type,
- Integer index)
- : d_type(new TypeNode(type)), d_index(index)
-{
- PrettyCheckArgument(type.isSort(),
- type,
- "uninterpreted constants can only be created for "
- "uninterpreted sorts, not `%s'",
- type.toString().c_str());
- PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
-}
-
-UninterpretedConstant::~UninterpretedConstant() {}
-
-UninterpretedConstant::UninterpretedConstant(const UninterpretedConstant& other)
- : d_type(new TypeNode(other.getType())), d_index(other.getIndex())
-{
-}
-
-const TypeNode& UninterpretedConstant::getType() const { return *d_type; }
-const Integer& UninterpretedConstant::getIndex() const { return d_index; }
-bool UninterpretedConstant::operator==(const UninterpretedConstant& uc) const
-{
- return getType() == uc.getType() && d_index == uc.d_index;
-}
-bool UninterpretedConstant::operator!=(const UninterpretedConstant& uc) const
-{
- return !(*this == uc);
-}
-
-bool UninterpretedConstant::operator<(const UninterpretedConstant& uc) const
-{
- return getType() < uc.getType()
- || (getType() == uc.getType() && d_index < uc.d_index);
-}
-bool UninterpretedConstant::operator<=(const UninterpretedConstant& uc) const
-{
- return getType() < uc.getType()
- || (getType() == uc.getType() && d_index <= uc.d_index);
-}
-bool UninterpretedConstant::operator>(const UninterpretedConstant& uc) const
-{
- return !(*this <= uc);
-}
-bool UninterpretedConstant::operator>=(const UninterpretedConstant& uc) const
-{
- return !(*this < uc);
-}
-
-std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
- std::stringstream ss;
- ss << uc.getType();
- std::string st(ss.str());
- // must remove delimiting quotes from the name of the type
- // this prevents us from printing symbols like |@uc_|T|_n|
- std::string q("|");
- size_t pos;
- while ((pos = st.find(q)) != std::string::npos)
- {
- st.replace(pos, 1, "");
- }
- return out << "uc_" << st.c_str() << "_" << uc.getIndex();
-}
-
-size_t UninterpretedConstantHashFunction::operator()(
- const UninterpretedConstant& uc) const
-{
- return std::hash<TypeNode>()(uc.getType())
- * IntegerHashFunction()(uc.getIndex());
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andres Noetzli, Morgan Deters, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Representation of constants of uninterpreted sorts.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__UNINTERPRETED_CONSTANT_H
-#define CVC5__UNINTERPRETED_CONSTANT_H
-
-#include <iosfwd>
-#include <memory>
-
-#include "util/integer.h"
-
-namespace cvc5 {
-
-class TypeNode;
-
-class UninterpretedConstant
-{
- public:
- UninterpretedConstant(const TypeNode& type, Integer index);
- ~UninterpretedConstant();
-
- UninterpretedConstant(const UninterpretedConstant& other);
-
- const TypeNode& getType() const;
- const Integer& getIndex() const;
- bool operator==(const UninterpretedConstant& uc) const;
- bool operator!=(const UninterpretedConstant& uc) const;
- bool operator<(const UninterpretedConstant& uc) const;
- bool operator<=(const UninterpretedConstant& uc) const;
- bool operator>(const UninterpretedConstant& uc) const;
- bool operator>=(const UninterpretedConstant& uc) const;
-
- private:
- std::unique_ptr<TypeNode> d_type;
- const Integer d_index;
-}; /* class UninterpretedConstant */
-
-std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc);
-
-/**
- * Hash function for the BitVector constants.
- */
-struct UninterpretedConstantHashFunction
-{
- size_t operator()(const UninterpretedConstant& uc) const;
-}; /* struct UninterpretedConstantHashFunction */
-
-} // namespace cvc5
-
-#endif /* CVC5__UNINTERPRETED_CONSTANT_H */
std::vector<api::Term> elements = d_solver->getModelDomainElements(s);
for (const api::Term& e : elements)
{
- // Uninterpreted constants are abstract values, which by SMT-LIB are
- // required to be annotated with their type, e.g. (as @uc_Foo_0 Foo).
- // Thus, the element is not printed simply as its name.
- std::string en = e.toString();
- size_t index = en.find("(as ");
- if (index == 0)
- {
- index = en.find(" ", 4);
- en = en.substr(4, index - 4);
- }
- Trace("parser") << "Get value scope : " << en << " -> " << e << std::endl;
- defineVar(en, e);
+ defineVar(e.getUninterpretedSortValue(), e);
}
}
}
return d_logicSet;
}
-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()) && strictModeEnabled())
&& name.find_first_not_of("0123456789", 1) == std::string::npos;
}
-api::Term Smt2::mkAbstractValue(const std::string& name)
-{
- Assert(isAbstractValue(name));
- // remove the '@'
- return d_solver->mkAbstractValue(name.substr(1));
-}
-
void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
{
Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
*/
api::Kind getIndexedOpKind(const std::string& name);
- /**
- * Returns the expression that name should be interpreted as.
- */
- api::Term getExpressionForNameAndType(const std::string& name,
- api::Sort t) override;
-
/**
* If we are in a version < 2.6, this updates name to the tester name of cons,
* e.g. "is-cons".
/** Make abstract value
*
* Abstract values are used for processing get-value calls. The argument
- * name should be such that isAbstractValue(name) is true.
+ * name should be such that isUninterpretedSortValue(name) is true.
*/
- api::Term mkAbstractValue(const std::string& name);
+ api::Term mkUninterpretedSortValue(const std::string& name);
/**
* Smt2 parser provides its own checkDeclaration, which does the
#include "expr/node_manager_attributes.h"
#include "expr/node_visitor.h"
#include "expr/sequence.h"
-#include "expr/uninterpreted_constant.h"
+#include "expr/skolem_manager.h"
#include "options/bv_options.h"
#include "options/language.h"
#include "options/printer_options.h"
#include "util/regexp.h"
#include "util/smt2_quote_string.h"
#include "util/string.h"
+#include "util/uninterpreted_sort_value.h"
using namespace std;
}
break;
}
-
- case kind::UNINTERPRETED_CONSTANT: {
- const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
+
+ case kind::UNINTERPRETED_SORT_VALUE:
+ {
+ const UninterpretedSortValue& av = n.getConst<UninterpretedSortValue>();
std::stringstream ss;
- ss << "(as @" << uc << " " << n.getType() << ")";
+ ss << "(as " << av << " " << n.getType() << ")";
out << ss.str();
break;
}
out << ")";
}
}
- else
+ else if (k != kind::UNINTERPRETED_SORT_VALUE)
{
// use type ascription
out << "(as ";
return;
}
- // variable
- if (n.isVar())
+ if (n.getKind() == kind::SKOLEM && nm->getSkolemManager()->isAbstractValue(n))
+ {
+ // abstract value
+ std::string s;
+ n.getAttribute(expr::VarNameAttr(), s);
+ out << "(as @" << cvc5::quoteSymbol(s) << " " << n.getType() << ")";
+ return;
+ }
+ else if (n.isVar())
{
+ // variable
string s;
if (n.getAttribute(expr::VarNameAttr(), s))
{
#include "smt/abstract_values.h"
#include "expr/ascription_type.h"
+#include "expr/skolem_manager.h"
#include "options/smt_options.h"
namespace cvc5 {
Node& val = d_abstractValues[n];
if (val.isNull())
{
- val = d_nm->mkAbstractValue(n.getType());
+ val = d_nm->getSkolemManager()->mkDummySkolem(
+ "a",
+ n.getType(),
+ "an abstract value",
+ SkolemManager::SKOLEM_ABSTRACT_VALUE);
d_abstractValueMap.addSubstitution(val, n);
}
- // We are supposed to ascribe types to all abstract values that go out.
- Node ascription = d_nm->mkConst(AscriptionType(n.getType()));
- Node retval = d_nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val);
- return retval;
+ return val;
}
} // namespace smt
#include "cvc5_private.h"
-#ifndef CVC5__SMT__ABSTRACT_VALUES_H
-#define CVC5__SMT__ABSTRACT_VALUES_H
+#ifndef CVC5__SMT__UNINTERPRETED_SORT_VALUES_H
+#define CVC5__SMT__UNINTERPRETED_SORT_VALUES_H
#include <unordered_map>
"::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" \
"theory/builtin/theory_builtin_type_rules.h"
-constant UNINTERPRETED_CONSTANT \
+constant UNINTERPRETED_SORT_VALUE \
class \
- UninterpretedConstant \
- ::cvc5::UninterpretedConstantHashFunction \
- "expr/uninterpreted_constant.h" \
- "the kind of expressions representing uninterpreted constants; payload is an instance of the cvc5::UninterpretedConstant class (used in models)"
-typerule UNINTERPRETED_CONSTANT ::cvc5::theory::builtin::UninterpretedConstantTypeRule
-enumerator SORT_TYPE \
- ::cvc5::theory::builtin::UninterpretedSortEnumerator \
- "theory/builtin/type_enumerator.h"
-
-constant ABSTRACT_VALUE \
- class \
- AbstractValue \
- ::cvc5::AbstractValueHashFunction \
- "util/abstract_value.h" \
- "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the cvc5::AbstractValue class (used in models)"
-typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule
+ UninterpretedSortValue \
+ ::cvc5::UninterpretedSortValueHashFunction \
+ "util/uninterpreted_sort_value.h" \
+ "the kind of expressions representing uninterpreted sort values; payload is an instance of the cvc5::AbstractValue class (used in models)"
+typerule UNINTERPRETED_SORT_VALUE ::cvc5::theory::builtin::UninterpretedSortValueTypeRule
+enumerator SORT_TYPE ::cvc5::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h"
# A kind representing "inlined" operators defined with OPERATOR
# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
#include "expr/attribute.h"
#include "expr/skolem_manager.h"
-#include "expr/uninterpreted_constant.h"
+#include "util/uninterpreted_sort_value.h"
namespace cvc5 {
namespace theory {
namespace builtin {
-TypeNode UninterpretedConstantTypeRule::computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
+TypeNode UninterpretedSortValueTypeRule::computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
{
- return n.getConst<UninterpretedConstant>().getType();
+ return n.getConst<UninterpretedSortValue>().getType();
}
/**
}
};/* class SExprTypeRule */
-class UninterpretedConstantTypeRule {
+class UninterpretedSortValueTypeRule
+{
public:
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
-};/* class UninterpretedConstantTypeRule */
-
-class AbstractValueTypeRule {
- public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
- // An UnknownTypeException means that this node has no type. For now,
- // only abstract values are like this---and then, only if they are created
- // by the user and don't actually correspond to one that the SolverEngine
- // gave them previously.
- throw UnknownTypeException(n);
- }
-};/* class AbstractValueTypeRule */
+}; /* class UninterpretedSortValueTypeRule */
class WitnessTypeRule
{
#include "theory/builtin/type_enumerator.h"
#include "theory/builtin/theory_builtin_rewriter.h"
+#include "util/uninterpreted_sort_value.h"
namespace cvc5 {
namespace theory {
throw NoMoreValuesException(getType());
}
return NodeManager::currentNM()->mkConst(
- UninterpretedConstant(getType(), d_count));
+ UninterpretedSortValue(getType(), d_count));
}
UninterpretedSortEnumerator& UninterpretedSortEnumerator::operator++()
#include "expr/kind.h"
#include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
#include "theory/type_enumerator.h"
#include "util/integer.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/datatypes/tuple_project_op.h"
#include "util/rational.h"
+#include "util/uninterpreted_sort_value.h"
using namespace cvc5;
using namespace cvc5::kind;
#include "expr/dtype.h"
#include "expr/kind.h"
#include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
#include "options/quantifiers_options.h"
#include "theory/type_enumerator.h"
new (&d_str) String;
d_str = other.d_str;
break;
- case UCONST:
- new (&d_uc)
- UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
- break;
+ case UVALUE: new (&d_av) UninterpretedSortValue(other.d_av); break;
case INVALID: break;
}
}
new (&d_str) String;
d_str = other.d_str;
break;
- case UCONST:
- new (&d_uc)
- UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
- break;
+ case UVALUE: new (&d_av) UninterpretedSortValue(other.d_av); break;
case INVALID: break;
}
}
d_str.~String();
break;
}
- case UCONST:
+ case UVALUE:
{
- d_uc.~UninterpretedConstant();
+ d_av.~UninterpretedSortValue();
break;
}
default: break;
case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
case EvalResult::RATIONAL: return nm->mkConst(CONST_RATIONAL, d_rat);
case EvalResult::STRING: return nm->mkConst(d_str);
- case EvalResult::UCONST: return nm->mkConst(d_uc);
+ case EvalResult::UVALUE: return nm->mkConst(d_av);
default:
{
Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
results[currNode] = EvalResult(r);
break;
}
- case kind::UNINTERPRETED_CONSTANT:
+ case kind::UNINTERPRETED_SORT_VALUE:
{
- const UninterpretedConstant& uc =
- currNodeVal.getConst<UninterpretedConstant>();
- results[currNode] = EvalResult(uc);
+ const UninterpretedSortValue& av =
+ currNodeVal.getConst<UninterpretedSortValue>();
+ results[currNode] = EvalResult(av);
break;
}
case kind::PLUS:
results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
break;
}
- case EvalResult::UCONST:
+ case EvalResult::UVALUE:
{
- results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc);
+ results[currNode] = EvalResult(lhs.d_av == rhs.d_av);
break;
}
#include "base/output.h"
#include "expr/node.h"
-#include "expr/uninterpreted_constant.h"
#include "util/bitvector.h"
#include "util/rational.h"
#include "util/string.h"
+#include "util/uninterpreted_sort_value.h"
namespace cvc5 {
namespace theory {
BITVECTOR,
RATIONAL,
STRING,
- UCONST,
+ UVALUE,
INVALID
} d_tag;
BitVector d_bv;
Rational d_rat;
String d_str;
- UninterpretedConstant d_uc;
+ UninterpretedSortValue d_av;
};
EvalResult(const EvalResult& other);
EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
- EvalResult(const UninterpretedConstant& u) : d_tag(UCONST), d_uc(u) {}
+ EvalResult(const UninterpretedSortValue& av) : d_tag(UVALUE), d_av(av) {}
EvalResult& operator=(const EvalResult& other);
{
// generate constant array over the first element of the constituent type
Node c = nm->mkGroundTerm(type);
- // note that c should never contain an uninterpreted constant
- Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c));
+ // note that c should never contain an uninterpreted sort value
+ Assert(!expr::hasSubtermKind(UNINTERPRETED_SORT_VALUE, c));
ops.push_back(c);
}
else if (type.isRoundingMode())
bool TermUtil::containsUninterpretedConstant( Node n ) {
if (!n.hasAttribute(ContainsUConstAttribute()) ){
bool ret = false;
- if( n.getKind()==UNINTERPRETED_CONSTANT ){
+ if (n.getKind() == UNINTERPRETED_SORT_VALUE && n.getType().isSort())
+ {
ret = true;
- }else{
+ }
+ else
+ {
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( containsUninterpretedConstant( n[i] ) ){
ret = true;
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
-#include "expr/uninterpreted_constant.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/strings_options.h"
#include "smt/env.h"
#include "theory/rewriter.h"
#include "theory/uf/theory_uf_model.h"
+#include "util/uninterpreted_sort_value.h"
using namespace std;
using namespace cvc5::kind;
unsigned card = eqc_usort_count[tn];
Trace("model-builder-debug") << " Cardinality is " << card << std::endl;
unsigned index =
- v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+ v.getConst<UninterpretedSortValue>().getIndex().toUnsignedInt();
Trace("model-builder-debug") << " Index is " << index << std::endl;
return index > 0 && index >= card;
}
case kind::COMBINED_CARDINALITY_CONSTRAINT:
//do nothing
break;
- case kind::UNINTERPRETED_CONSTANT:
+ case kind::UNINTERPRETED_SORT_VALUE:
{
- // Uninterpreted constants should only appear in models, and should
- // never appear in constraints. They are unallowed to ever appear in
- // constraints since the cardinality of an uninterpreted sort may have
- // an upper bound, e.g. if (forall ((x U) (y U)) (= x y)) holds, then
- // @uc_U_2 is a ill-formed term, as its existence cannot be assumed.
- // The parser prevents the user from ever constructing uninterpreted
- // constants. However, they may be exported via models to API users.
- // It is thus possible that these uninterpreted constants are asserted
- // back in constraints, hence this check is necessary.
+ // Uninterpreted sort values should only appear in models, and should never
+ // appear in constraints. They are unallowed to ever appear in constraints
+ // since the cardinality of an uninterpreted sort may have an upper bound,
+ // e.g. if (forall ((x U) (y U)) (= x y)) holds, then @uc_U_2 is a
+ // ill-formed term, as its existence cannot be assumed. The parser
+ // prevents the user from ever constructing uninterpreted sort values.
+ // However, they may be exported via models to API users. It is thus
+ // possible that these uninterpreted sort values are asserted back in
+ // constraints, hence this check is necessary.
throw LogicException(
"An uninterpreted constant was preregistered to the UF theory.");
}
configure_file(real_algebraic_number.h.in real_algebraic_number.h)
libcvc5_add_sources(
- abstract_value.cpp
- abstract_value.h
bin_heap.h
bitvector.cpp
bitvector.h
statistics_value.h
string.cpp
string.h
+ uninterpreted_sort_value.cpp
+ uninterpreted_sort_value.h
unsafe_interrupt_exception.h
utility.cpp
utility.h
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Tim King, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Representation of abstract values.
- */
-
-#include "util/abstract_value.h"
-
-#include <iostream>
-#include <sstream>
-#include <string>
-
-#include "base/check.h"
-
-using namespace std;
-
-namespace cvc5 {
-
-std::ostream& operator<<(std::ostream& out, const AbstractValue& val) {
- return out << "@" << val.getIndex();
-}
-
-AbstractValue::AbstractValue(Integer index) : d_index(index)
-{
- PrettyCheckArgument(index >= 1,
- index,
- "index >= 1 required for abstract value, not `%s'",
- index.toString().c_str());
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Tim King, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Representation of abstract values.
- */
-
-#include "cvc5_public.h"
-
-#pragma once
-
-#include <iosfwd>
-
-#include "util/integer.h"
-
-namespace cvc5 {
-
-class AbstractValue
-{
- const Integer d_index;
-
- public:
- AbstractValue(Integer index);
-
- const Integer& getIndex() const { return d_index; }
- bool operator==(const AbstractValue& val) const
- {
- return d_index == val.d_index;
- }
- bool operator!=(const AbstractValue& val) const { return !(*this == val); }
- bool operator<(const AbstractValue& val) const
- {
- return d_index < val.d_index;
- }
- bool operator<=(const AbstractValue& val) const
- {
- return d_index <= val.d_index;
- }
- bool operator>(const AbstractValue& val) const { return !(*this <= val); }
- bool operator>=(const AbstractValue& val) const { return !(*this < val); }
-}; /* class AbstractValue */
-
-std::ostream& operator<<(std::ostream& out, const AbstractValue& val);
-
-/**
- * Hash function for the BitVector constants.
- */
-struct AbstractValueHashFunction
-{
- inline size_t operator()(const AbstractValue& val) const {
- return IntegerHashFunction()(val.getIndex());
- }
-}; /* struct AbstractValueHashFunction */
-
-} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Tim King, Morgan Deters
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Representation of abstract values.
+ */
+
+#include "util/uninterpreted_sort_value.h"
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "base/check.h"
+#include "expr/type_node.h"
+
+using namespace std;
+
+namespace cvc5 {
+
+std::ostream& operator<<(std::ostream& out, const UninterpretedSortValue& val)
+{
+ return out << "@a" << val.getIndex();
+}
+
+UninterpretedSortValue::UninterpretedSortValue(const TypeNode& type,
+ const Integer& index)
+ : d_type(new TypeNode(type)), d_index(index)
+{
+ PrettyCheckArgument(type.isSort(),
+ type,
+ "uninterpreted constants can only be created for "
+ "uninterpreted sorts, not `%s'",
+ type.toString().c_str());
+ PrettyCheckArgument(index >= 0,
+ index,
+ "index >= 0 required for abstract value, not `%s'",
+ index.toString().c_str());
+}
+
+UninterpretedSortValue::UninterpretedSortValue(
+ const UninterpretedSortValue& val)
+ : d_type(new TypeNode(*val.d_type)), d_index(val.d_index)
+{
+}
+
+UninterpretedSortValue::~UninterpretedSortValue() {}
+
+const TypeNode& UninterpretedSortValue::getType() const { return *d_type; }
+
+bool UninterpretedSortValue::operator==(const UninterpretedSortValue& val) const
+{
+ return getType() == val.getType() && d_index == val.d_index;
+}
+
+bool UninterpretedSortValue::operator<(const UninterpretedSortValue& val) const
+{
+ return getType() < val.getType()
+ || (getType() == val.getType() && d_index < val.d_index);
+}
+
+bool UninterpretedSortValue::operator<=(const UninterpretedSortValue& val) const
+{
+ return getType() <= val.getType()
+ || (getType() == val.getType() && d_index <= val.d_index);
+}
+
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Morgan Deters, Tim King, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Representation of abstract values.
+ */
+
+#include "cvc5_public.h"
+
+#pragma once
+
+#include <iosfwd>
+#include <memory>
+
+#include "util/integer.h"
+
+namespace cvc5 {
+
+class TypeNode;
+
+class UninterpretedSortValue
+{
+ public:
+ UninterpretedSortValue(const TypeNode& type, const Integer& index);
+ UninterpretedSortValue(const UninterpretedSortValue& val);
+ ~UninterpretedSortValue();
+
+ const Integer& getIndex() const { return d_index; }
+ const TypeNode& getType() const;
+
+ bool operator==(const UninterpretedSortValue& val) const;
+ bool operator!=(const UninterpretedSortValue& val) const
+ {
+ return !(*this == val);
+ }
+ bool operator<(const UninterpretedSortValue& val) const;
+ bool operator<=(const UninterpretedSortValue& val) const;
+ bool operator>(const UninterpretedSortValue& val) const
+ {
+ return !(*this <= val);
+ }
+ bool operator>=(const UninterpretedSortValue& val) const
+ {
+ return !(*this < val);
+ }
+
+ private:
+ /** The type of the abstract value */
+ std::unique_ptr<TypeNode> d_type;
+ /** The index of the abstract value */
+ const Integer d_index;
+}; /* class UninterpretedSortValue */
+
+std::ostream& operator<<(std::ostream& out, const UninterpretedSortValue& val);
+
+/**
+ * Hash function for abstract values.
+ */
+struct UninterpretedSortValueHashFunction
+{
+ inline size_t operator()(const UninterpretedSortValue& val) const
+ {
+ return IntegerHashFunction()(val.getIndex());
+ }
+}; /* struct UninterpretedSortValueHashFunction */
+
+} // namespace cvc5
; COMMAND-LINE: --incremental --abstract-values
; EXPECT: sat
-; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int))))
+; EXPECT: ((a (as @a_2 (Array Int Int))) (b (as @a_3 (Array Int Int))))
(set-logic QF_AUFLIA)
(set-option :produce-models true)
(declare-fun a () (Array Int Int))
;
; COMMAND-LINE: --incremental --abstract-values --check-models
; EXPECT: sat
-; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int))))
+; EXPECT: ((a (as @a_2 (Array Int Int))) (b (as @a_3 (Array Int Int))))
(set-logic QF_AUFLIA)
(set-option :produce-models true)
(declare-fun a () (Array Int Int))
; COMMAND-LINE: --produce-models
; EXPECT: sat
-; EXPECT: (((f (as @uc_Foo_0 Foo)) 3))
+; EXPECT: (((f (as @a0 Foo)) 3))
(set-logic ALL)
(set-option :produce-models true)
(declare-sort Foo 0)
(declare-fun f (Foo) Int)
(assert (exists ((x Foo)) (= (f x) 3)))
(check-sat)
-(get-value ((f @uc_Foo_0)))
+(get-value ((f @a0)))
ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
}
-TEST_F(TestApiBlackSolver, mkAbstractValue)
-{
- ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1")));
- ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC5ApiException);
- ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC5ApiException);
- ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC5ApiException);
- ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC5ApiException);
- ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC5ApiException);
-
- ASSERT_NO_THROW(d_solver.mkAbstractValue((uint32_t)1));
- ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)1));
- ASSERT_NO_THROW(d_solver.mkAbstractValue((uint64_t)1));
- ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)1));
- ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)-1));
- ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)-1));
- ASSERT_THROW(d_solver.mkAbstractValue(0), CVC5ApiException);
-}
-
TEST_F(TestApiBlackSolver, mkFloatingPoint)
{
Term t1 = d_solver.mkBitVector(8);
ASSERT_EQ("f", b7.getBitVectorValue(16));
}
-TEST_F(TestApiBlackTerm, getAbstractValue)
+TEST_F(TestApiBlackTerm, getUninterpretedSortValue)
{
- Term v1 = d_solver.mkAbstractValue(1);
- Term v2 = d_solver.mkAbstractValue("15");
- Term v3 = d_solver.mkAbstractValue("18446744073709551617");
-
- ASSERT_TRUE(v1.isAbstractValue());
- ASSERT_TRUE(v2.isAbstractValue());
- ASSERT_TRUE(v3.isAbstractValue());
- ASSERT_EQ("1", v1.getAbstractValue());
- ASSERT_EQ("15", v2.getAbstractValue());
- ASSERT_EQ("18446744073709551617", v3.getAbstractValue());
+ d_solver.setOption("produce-models", "true");
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ Term x = d_solver.mkConst(uSort, "x");
+ Term y = d_solver.mkConst(uSort, "y");
+ d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y));
+ ASSERT_TRUE(d_solver.checkSat().isSat());
+ Term vx = d_solver.getValue(x);
+ Term vy = d_solver.getValue(y);
+ ASSERT_TRUE(vx.isUninterpretedSortValue());
+ ASSERT_TRUE(vy.isUninterpretedSortValue());
+ ASSERT_EQ(vx.getUninterpretedSortValue(), vy.getUninterpretedSortValue());
}
TEST_F(TestApiBlackTerm, getTuple)
ASSERT_EQ(std::vector<Term>({i1, i1, i2}), s5.getSequenceValue());
}
-TEST_F(TestApiBlackTerm, getUninterpretedConst)
-{
- Sort s = d_solver.mkUninterpretedSort("test");
- Term t1 = d_solver.mkUninterpretedConst(s, 3);
- Term t2 = d_solver.mkUninterpretedConst(s, 5);
-
- ASSERT_TRUE(t1.isUninterpretedValue());
- ASSERT_TRUE(t2.isUninterpretedValue());
-
- ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue());
- ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue());
-}
-
TEST_F(TestApiBlackTerm, substitute)
{
Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO));
}
- @Test void mkAbstractValue() throws CVC5ApiException
- {
- assertDoesNotThrow(() -> d_solver.mkAbstractValue(("1")));
- assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("0")));
- assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("-1")));
- assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("1.2")));
- assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("1/2"));
- assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("asdf"));
-
- assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1));
- assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1));
- assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1));
- assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1));
- // java does not have specific types for unsigned integers, therefore the two lines below do not
- // make sense in java. assertDoesNotThrow(() -> d_solver.mkAbstractValue((int)-1));
- // assertDoesNotThrow(() -> d_solver.mkAbstractValue((long)-1));
- assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(0));
- }
-
@Test void mkFloatingPoint() throws CVC5ApiException
{
Term t1 = d_solver.mkBitVector(8);
assertEquals("f", b7.getBitVectorValue(16));
}
- @Test void getAbstractValue() throws CVC5ApiException
+ @Test void getUninterpretedSortValue() throws CVC5ApiException
{
- Term v1 = d_solver.mkAbstractValue(1);
- Term v2 = d_solver.mkAbstractValue("15");
- Term v3 = d_solver.mkAbstractValue("18446744073709551617");
-
- assertTrue(v1.isAbstractValue());
- assertTrue(v2.isAbstractValue());
- assertTrue(v3.isAbstractValue());
- assertEquals("1", v1.getAbstractValue());
- assertEquals("15", v2.getAbstractValue());
- assertEquals("18446744073709551617", v3.getAbstractValue());
+ d_solver.setOption("produce-models", "true");
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ Term x = d_solver.mkConst(uSort, "x");
+ Term y = d_solver.mkConst(uSort, "y");
+ d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y));
+ assertTrue(d_solver.checkSat().isSat());
+ Term vx = d_solver.getValue(x);
+ Term vy = d_solver.getValue(y);
+ assertEquals(vx.isUninterpretedSortValue(), vy.isUninterpretedSortValue());
+ assertDoesNotThrow(() -> vx.getUninterpretedSortValue());
+ assertDoesNotThrow(() -> vy.getUninterpretedSortValue());
}
@Test void getTuple()
assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue()));
}
- @Test void getUninterpretedConst() throws CVC5ApiException
- {
- Sort s = d_solver.mkUninterpretedSort("test");
- Term t1 = d_solver.mkUninterpretedConst(s, 3);
- Term t2 = d_solver.mkUninterpretedConst(s, 5);
-
- assertTrue(t1.isUninterpretedValue());
- assertTrue(t2.isUninterpretedValue());
-
- assertEquals(new Pair<Sort, Integer>(s, 3), t1.getUninterpretedValue());
- assertEquals(new Pair<Sort, Integer>(s, 5), t2.getUninterpretedValue());
- }
-
@Test void substitute()
{
Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
solver.mkRoundingMode(pycvc5.RoundTowardZero)
-def test_mk_abstract_value(solver):
- solver.mkAbstractValue("1")
- with pytest.raises(ValueError):
- solver.mkAbstractValue("0")
- with pytest.raises(ValueError):
- solver.mkAbstractValue("-1")
- with pytest.raises(ValueError):
- solver.mkAbstractValue("1.2")
- with pytest.raises(ValueError):
- solver.mkAbstractValue("1/2")
- with pytest.raises(ValueError):
- solver.mkAbstractValue("asdf")
-
- solver.mkAbstractValue(1)
- with pytest.raises(ValueError):
- solver.mkAbstractValue(-1)
- with pytest.raises(ValueError):
- solver.mkAbstractValue(0)
-
-
def test_mk_floating_point(solver):
t1 = solver.mkBitVector(8)
t2 = solver.mkBitVector(4)
assert one == constarr.getConstArrayBase()
-def test_get_abstract_value(solver):
- v1 = solver.mkAbstractValue(1)
- v2 = solver.mkAbstractValue("15")
- v3 = solver.mkAbstractValue("18446744073709551617")
-
- assert v1.isAbstractValue()
- assert v2.isAbstractValue()
- assert v3.isAbstractValue()
- assert "1" == v1.getAbstractValue()
- assert "15" == v2.getAbstractValue()
- assert "18446744073709551617" == v3.getAbstractValue()
+def test_get_uninterpreted_sort_value(solver):
+ solver.setOption("produce-models", "true")
+ uSort = solver.mkUninterpretedSort("u")
+ x = solver.mkConst(uSort, "x")
+ y = solver.mkConst(uSort, "y")
+ solver.assertFormula(solver.mkTerm(Kind.Equal, x, y))
+ assert solver.checkSat().isSat()
+ vx = solver.getValue(x)
+ vy = solver.getValue(y)
+ assert vx.isUninterpretedSortValue()
+ assert vy.isUninterpretedSortValue()
+ assert vx.getUninterpretedSortValue() == vy.getUninterpretedSortValue()
def test_get_tuple(solver):
assert [i1, i1, i2] == s5.getSequenceValue()
-def test_get_uninterpreted_const(solver):
- s = solver.mkUninterpretedSort("test")
- t1 = solver.mkUninterpretedConst(s, 3)
- t2 = solver.mkUninterpretedConst(s, 5)
-
- assert t1.isUninterpretedValue()
- assert t2.isUninterpretedValue()
-
- assert (s, 3) == t1.getUninterpretedValue()
- assert (s, 5) == t2.getUninterpretedValue()
-
-
def test_get_floating_point(solver):
bvval = solver.mkBitVector(16, "0000110000000011", 2)
fp = solver.mkFloatingPoint(5, 11, bvval)
#include "expr/dtype.h"
#include "expr/kind.h"
#include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
#include "options/language.h"
#include "test_smt.h"
#include "theory/type_enumerator.h"
#include "util/bitvector.h"
#include "util/rational.h"
+#include "util/uninterpreted_sort_value.h"
namespace cvc5 {
TypeNode sort = d_nodeManager->mkSort("T");
TypeNode sort2 = d_nodeManager->mkSort("U");
TypeEnumerator te(sort);
- ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, 0)));
+ ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedSortValue(sort, 0)));
for (size_t i = 1; i < 100; ++i)
{
- ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i)));
- ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort2, i)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedConstant(sort, i)));
- ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i + 2)));
+ ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedSortValue(sort, i)));
+ ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedSortValue(sort2, i)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedSortValue(sort, i)));
+ ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedSortValue(sort, i + 2)));
}
}
*/
#include "expr/array_store_all.h"
-#include "expr/uninterpreted_constant.h"
#include "test_smt.h"
#include "util/rational.h"
+#include "util/uninterpreted_sort_value.h"
using namespace cvc5::kind;
d_nodeManager->realType()),
d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2)));
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort),
- d_nodeManager->mkConst(UninterpretedConstant(usort, 0)));
+ d_nodeManager->mkConst(UninterpretedSortValue(usort, 0)));
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
d_nodeManager->realType()),
d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
TEST_F(TestUtilWhiteArrayStoreAll, type_errors)
{
ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
- d_nodeManager->mkConst(UninterpretedConstant(
+ d_nodeManager->mkConst(UninterpretedSortValue(
d_nodeManager->mkSort("U"), 0))),
IllegalArgumentException);
ASSERT_THROW(
projects / cvc5.git / commitdiff