From 4c428c8f74ae913f05287c0595c8887c31089520 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 11 Jul 2011 18:48:16 +0000 Subject: [PATCH] if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as well as pre-registration of free constants of uninterpreted sort, etc.. --- src/theory/theory_engine.cpp | 18 ++++++----- src/theory/theory_engine.h | 30 +++++++++++++++++-- test/regress/regress0/arrays/Makefile.am | 7 +++-- .../regress0/arrays/incorrect2.minimized.smt | 2 +- .../regress0/arrays/incorrect8.minimized.smt | 20 +++++++++++++ 5 files changed, 63 insertions(+), 14 deletions(-) create mode 100644 test/regress/regress0/arrays/incorrect8.minimized.smt diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4237e0992..3571171f8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -182,7 +182,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { preregister_stack_element& stackHead = toVisit.back(); // The current node we are processing TNode current = stackHead.node; - // If we already added all the children its time to register or just pop from the stack + // If we already added all the children its time to register or just + // pop from the stack if (stackHead.children_added || current.getAttribute(PreRegistered())) { if (!current.getAttribute(PreRegistered())) { // Mark it as registered @@ -194,18 +195,21 @@ void TheoryEngine::preRegister(TNode preprocessed) { } else { Theory* theory = theoryOf(current); TheoryId theoryLHS = theory->getId(); - Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; + Debug("register") << "preregistering " << current + << " with " << theoryLHS << std::endl; markActive(theoryLHS); theory->preRegisterTerm(current); } } else { - TheoryId theory = Theory::theoryOf(current); - Debug("register") << "preregistering " << current << " with " << theory << std::endl; + TheoryId theory = theoryIdOf(current); + Debug("register") << "preregistering " << current + << " with " << theory << std::endl; markActive(theory); d_theoryTable[theory]->preRegisterTerm(current); - TheoryId typeTheory = Theory::theoryOf(current.getType()); + TheoryId typeTheory = theoryIdOf(current.getType()); if (theory != typeTheory) { - Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; + Debug("register") << "preregistering " << current + << " with " << typeTheory << std::endl; markActive(typeTheory); d_theoryTable[typeTheory]->preRegisterTerm(current); } @@ -408,7 +412,7 @@ Node TheoryEngine::preprocess(TNode assertion) { } // If this is an atom, we preprocess it with the theory - if (Theory::theoryOf(current) != THEORY_BOOL) { + if (theoryIdOf(current) != THEORY_BOOL) { d_atomPreprocessingCache[current] = theoryOf(current)->preprocess(current); continue; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5b724a7c7..94ba8cabb 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -290,12 +290,24 @@ public: */ inline theory::Theory* theoryOf(TNode node) { if (node.getKind() == kind::EQUAL) { - return d_theoryTable[theory::Theory::theoryOf(node[0])]; + return d_theoryTable[theoryIdOf(node[0])]; } else { - return d_theoryTable[theory::Theory::theoryOf(node)]; + return d_theoryTable[theoryIdOf(node)]; } } + /** + * Wrapper for theory::Theory::theoryOf() that implements the + * array/EUF hack. + */ + inline theory::TheoryId theoryIdOf(TNode node) { + theory::TheoryId id = theory::Theory::theoryOf(node); + if(d_logic == "QF_AX" && id == theory::THEORY_UF) { + id = theory::THEORY_ARRAY; + } + return id; + } + /** * Get the theory associated to a given Node. * @@ -303,7 +315,19 @@ public: * of built-in type. */ inline theory::Theory* theoryOf(const TypeNode& typeNode) { - return d_theoryTable[theory::Theory::theoryOf(typeNode)]; + return d_theoryTable[theoryIdOf(typeNode)]; + } + + /** + * Wrapper for theory::Theory::theoryOf() that implements the + * array/EUF hack. + */ + inline theory::TheoryId theoryIdOf(const TypeNode& typeNode) { + theory::TheoryId id = theory::Theory::theoryOf(typeNode); + if(d_logic == "QF_AX" && id == theory::THEORY_UF) { + id = theory::THEORY_ARRAY; + } + return id; } /** diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index e3b30827c..b7a60917b 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -8,9 +8,7 @@ TESTS = \ arrays1.smt2 \ arrays2.smt2 \ arrays3.smt2 \ - arrays4.smt2 - -EXTRA_DIST = $(TESTS) \ + arrays4.smt2 \ incorrect1.smt \ incorrect2.smt \ incorrect2.minimized.smt \ @@ -20,10 +18,13 @@ EXTRA_DIST = $(TESTS) \ incorrect6.smt \ incorrect7.smt \ incorrect8.smt \ + incorrect8.minimized.smt \ incorrect9.smt \ incorrect10.smt \ incorrect11.smt +EXTRA_DIST = $(TESTS) + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ diff --git a/test/regress/regress0/arrays/incorrect2.minimized.smt b/test/regress/regress0/arrays/incorrect2.minimized.smt index aa803d060..6bb3bbfd8 100644 --- a/test/regress/regress0/arrays/incorrect2.minimized.smt +++ b/test/regress/regress0/arrays/incorrect2.minimized.smt @@ -3,7 +3,7 @@ :extrafuns ((v3 Index)) :extrafuns ((v4 Index)) :extrafuns ((v2 Index)) -:status unknown +:status unsat :formula (flet ($n1 true) (flet ($n2 (= v4 v3)) diff --git a/test/regress/regress0/arrays/incorrect8.minimized.smt b/test/regress/regress0/arrays/incorrect8.minimized.smt new file mode 100644 index 000000000..18067e654 --- /dev/null +++ b/test/regress/regress0/arrays/incorrect8.minimized.smt @@ -0,0 +1,20 @@ +(benchmark fuzzsmt +:logic QF_AX +:extrafuns ((v4 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v5 Element)) +:extrafuns ((v1 Array)) +:status unknown +:formula +(let (?n1 (store v1 v4 v5)) +(let (?n2 (select ?n1 v3)) +(let (?n3 (select v1 v3)) +(flet ($n4 (distinct ?n2 ?n3)) +(let (?n5 (ite $n4 v4 v3)) +(let (?n6 (store ?n1 v4 v5)) +(let (?n7 (select ?n6 v3)) +(flet ($n8 (= ?n2 ?n7)) +(let (?n9 (ite $n8 v3 v4)) +(flet ($n10 (distinct ?n5 ?n9)) +$n10 +))))))))))) -- 2.30.2