Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
return fact;
}
- /**
- * Provides access to the facts queue, primarily intended for theory
- * debugging purposes.
- *
- * @return the iterator to the beginning of the fact queue
- */
- context::CDList<Assertion>::const_iterator facts_begin() const {
- return d_facts.begin();
- }
-
- /**
- * Provides access to the facts queue, primarily intended for theory
- * debugging purposes.
- *
- * @return the iterator to the end of the fact queue
- */
- context::CDList<Assertion>::const_iterator facts_end() const {
- return d_facts.end();
- }
-
/**
* The theory that owns the uninterpreted sort.
*/
return ss.str();
}
+ /**
+ * Provides access to the facts queue, primarily intended for theory
+ * debugging purposes.
+ *
+ * @return the iterator to the beginning of the fact queue
+ */
+ context::CDList<Assertion>::const_iterator facts_begin() const {
+ return d_facts.begin();
+ }
+
+ /**
+ * Provides access to the facts queue, primarily intended for theory
+ * debugging purposes.
+ *
+ * @return the iterator to the end of the fact queue
+ */
+ context::CDList<Assertion>::const_iterator facts_end() const {
+ return d_facts.end();
+ }
+
+ /**
+ * Provides access to the shared terms, primarily intended for theory
+ * debugging purposes.
+ *
+ * @return the iterator to the beginning of the shared terms list
+ */
+ context::CDList<TNode>::const_iterator shared_terms_begin() const {
+ return d_sharedTerms.begin();
+ }
+
+ /**
+ * Provides access to the facts queue, primarily intended for theory
+ * debugging purposes.
+ *
+ * @return the iterator to the end of the shared terms list
+ */
+ context::CDList<TNode>::const_iterator shared_terms_end() const {
+ return d_sharedTerms.end();
+ }
+
};/* class Theory */
std::ostream& operator<<(std::ostream& os, Theory::Effort level);
Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
+ if (Debug.isOn("theory::assertions")) {
+ for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++ theoryId) {
+ Theory* theory = d_theoryTable[theoryId];
+ if (theory && Theory::setContains((TheoryId)theoryId, d_activeTheories)) {
+ Debug("theory::assertions") << "--------------------------------------------" << std::endl;
+ Debug("theory::assertions") << "Assertions of " << theory->getId() << ": " << std::endl;
+ context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+ for (unsigned i = 0; it != it_end; ++ it, ++i) {
+ if ((*it).isPreregistered) {
+ Debug("theory::assertions") << "[" << i << "]: ";
+ } else {
+ Debug("theory::assertions") << "(" << i << "): ";
+ }
+ Debug("theory::assertions") << (*it).assertion << endl;
+ }
+
+ if (d_sharedTermsExist) {
+ Debug("theory::assertions") << "Shared terms of " << theory->getId() << ": " << std::endl;
+ context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
+ for (unsigned i = 0; it != it_end; ++ it, ++i) {
+ Debug("theory::assertions") << "[" << i << "]: " << (*it) << endl;
+ }
+ }
+ }
+ }
+ }
+
// Do the checking
CVC4_FOR_EACH_THEORY;
/** A context-dependents count of nodes */
context::CDO<size_t> d_nodesCount;
+ /**
+ * At time of addition a function application can already normalize to something, so
+ * we keep both the original, and the normalized version.
+ */
+ struct FunctionApplicationPair {
+ FunctionApplication original;
+ FunctionApplication normalized;
+ FunctionApplicationPair() {}
+ FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized)
+ : original(original), normalized(normalized) {}
+ bool isNull() const {
+ return !original.isApplication();
+ }
+ };
/** Map from ids to the applications */
- std::vector<FunctionApplication> d_applications;
+ std::vector<FunctionApplicationPair> d_applications;
/** Map from ids to the equality nodes */
std::vector<EqualityNode> d_equalityNodes;
// Get another id for this
EqualityNodeId funId = newNode(original, true);
- // The function application we're creating
+ FunctionApplication funOriginal(t1, t2);
+ // The function application we're creating
EqualityNodeId t1ClassId = getEqualityNode(t1).getFind();
EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
FunctionApplication funNormalized(t1ClassId, t2ClassId);
- // We add the normalized version, the term needs to be re-added on each backtrack
- d_applications[funId] = funNormalized;
+ // We add the original version
+ d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized);
// Add the lookup data, if it's not already there
typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
// Add the node to it's position
d_nodes.push_back(node);
// Note if this is an application or not
- d_applications.push_back(FunctionApplication());
+ d_applications.push_back(FunctionApplicationPair());
// Add the trigger list for this node
d_nodeTriggers.push_back(+null_trigger);
// Add it to the equality graph
// Get the function application
EqualityNodeId funId = useNode.getApplicationId();
Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
- const FunctionApplication& fun = d_applications[useNode.getApplicationId()];
+ const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
// Check if there is an application with find arguments
EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl;
d_nodeIds.erase(d_nodes[i]);
- const FunctionApplication& app = d_applications[i];
+ const FunctionApplication& app = d_applications[i].normalized;
if (app.isApplication()) {
// Remove b from use-list
getEqualityNode(app.b).removeTopFromUseList(d_useListNodes);
if (reasonType == MERGED_THROUGH_CONGRUENCE) {
// f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl;
- const FunctionApplication& f1 = d_applications[currentNode];
- const FunctionApplication& f2 = d_applications[edgeNode];
+ const FunctionApplication& f1 = d_applications[currentNode].original;
+ const FunctionApplication& f2 = d_applications[edgeNode].original;
Debug("equality") << push;
getExplanation(f1.a, f2.a, equalities);
getExplanation(f1.b, f2.b, equalities);
bug187.smt2 \
bug220.smt2 \
bug239.smt \
- buggy-ite.smt2
+ buggy-ite.smt2 \
+ bug303.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
--- /dev/null
+(set-logic QF_LIA)
+(set-info :status unsat)
+
+;; don't use a datatypes for currently focusing in uf
+(declare-sort list 0)
+
+(declare-fun cons (Int list) list)
+(declare-fun nil () list)
+
+;;define length
+(declare-fun length (list) Int)
+
+(assert (= (length nil) 0))
+
+(declare-fun one_cons (list) list)
+
+(assert (= (length (cons 1 nil)) (+ 1 (length nil))))
+(assert (= (one_cons nil) (cons 1 nil)))
+(assert (not (= (length (one_cons nil)) 1)))
+
+(check-sat)
+
+(exit)
projects / cvc5.git / commitdiff