diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-07 19:03:09 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-07 19:03:09 -0500 |
commit | 4908c52200a80a848dc529cc312aa5418f6d3dee (patch) | |
tree | 09713f463f0614b70d136d62b0b25256a4c2b053 | |
parent | a72276859f0af0f5e800434879eca111d8bf6644 (diff) | |
parent | 63ca7c0a10dcd6b3be42d4d513f842db76733392 (diff) |
Merge branch '1.0.x'
Conflicts:
src/theory/quantifiers/theory_quantifiers.cpp
-rw-r--r-- | src/Makefile.am | 6 | ||||
-rw-r--r-- | src/expr/expr_template.h | 17 | ||||
-rw-r--r-- | src/expr/options | 4 | ||||
-rw-r--r-- | src/expr/options_handlers.h | 3 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 4 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 83 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 6 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 37 | ||||
-rw-r--r-- | src/theory/substitutions.h | 6 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/bug484.smt2 | 111 |
12 files changed, 234 insertions, 53 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 40d3823e9..1d54bc2a8 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -120,7 +120,7 @@ install-data-local: (cd "$(srcdir)" && find * -name '*.h' | \ xargs grep -l '^# *include *"cvc4.*_public\.h"')) | \ while read f; do \ - if expr "$$f" : ".*_\(template\|private\|test_utils\)\.h$$" &>/dev/null; then \ + if expr "$$f" : ".*_\(template\|private\|private_library\|test_utils\)\.h$$" &>/dev/null; then \ continue; \ fi; \ d="$$(echo "$$f" | sed 's,^include/,,')"; \ @@ -150,7 +150,7 @@ uninstall-local: (cd "$(srcdir)" && find * -name '*.h' | \ xargs grep -l '^# *include *"cvc4.*_public\.h"')) | \ while read f; do \ - if expr "$$f" : ".*_\(template\|private\|test_utils\)\.h$$" &>/dev/null; then \ + if expr "$$f" : ".*_\(template\|private\|private_library\|test_utils\)\.h$$" &>/dev/null; then \ continue; \ fi; \ d="$$(echo "$$f" | sed 's,^include/,,')"; \ @@ -175,7 +175,7 @@ mostlyclean-local: (cd "$(srcdir)" && find * -name '*.h' | \ xargs grep -l '^# *include *"cvc4.*_public\.h"')) | \ while read f; do \ - if expr "$$f" : ".*_\(template\|private\|test_utils\)\.h$$" &>/dev/null; then \ + if expr "$$f" : ".*_\(template\|private\|private_library\|test_utils\)\.h$$" &>/dev/null; then \ continue; \ fi; \ d="$$(echo "$$f" | sed 's,^include/,,')"; \ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index b353ec5dc..f5df63f8c 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -654,6 +654,11 @@ public: l = options::defaultExprDepth(); } if(l == 0) { + // if called from outside the library, we may not have options + // available to us at this point (or perhaps the output language + // is not set in Options). Default to something reasonable, but + // don't set "l" since that would make it "sticky" for this + // stream. return s_defaultPrintDepth; } } @@ -797,7 +802,17 @@ public: if(l == 0) { // set the default dag setting on this ostream // (offset by one to detect whether default has been set yet) - l = s_defaultDag + 1; + if(&Options::current() != NULL) { + l = options::defaultDagThresh() + 1; + } + if(l == 0) { + // if called from outside the library, we may not have options + // available to us at this point (or perhaps the output language + // is not set in Options). Default to something reasonable, but + // don't set "l" since that would make it "sticky" for this + // stream. + return s_defaultDag + 1; + } } return static_cast<size_t>(l - 1); } diff --git a/src/expr/options b/src/expr/options index cd59e4875..223189d1b 100644 --- a/src/expr/options +++ b/src/expr/options @@ -5,9 +5,9 @@ module EXPR "expr/options.h" Expression package -option defaultExprDepth --default-expr-depth=N int :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h" +option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h" print exprs to depth N (0 == default, -1 == no limit) -option - default-dag-thresh --default-dag-thresh=N argument :handler CVC4::expr::setDefaultDagThresh :handler-include "expr/options_handlers.h" +option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::expr::setDefaultDagThresh :predicate-include "expr/options_handlers.h" dagify common subexprs appearing > N times (1 == default, 0 == don't dagify) option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h" print types with variables when printing exprs diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h index 7a1d73c36..57c4d1aa4 100644 --- a/src/expr/options_handlers.h +++ b/src/expr/options_handlers.h @@ -39,8 +39,7 @@ inline void setDefaultExprDepth(std::string option, int depth, SmtEngine* smt) { // intentionally exclude Dump stream from this list } -inline void setDefaultDagThresh(std::string option, std::string optarg, SmtEngine* smt) { - int dag = atoi(optarg.c_str()); +inline void setDefaultDagThresh(std::string option, int dag, SmtEngine* smt) { if(dag < 0) { throw OptionException("--default-dag-thresh requires a nonnegative argument."); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0f0012971..2ba1ae7a9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3338,6 +3338,7 @@ void SmtEngine::checkModel(bool hardFailure) { hash_map<Node, Node, NodeHashFunction> cache; n = d_private->expandDefinitions(n, cache); } + Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl; // Apply our model value substitutions. n = substitutions.apply(n); @@ -3359,6 +3360,12 @@ void SmtEngine::checkModel(bool hardFailure) { continue; } + // As a last-ditch effort, ask model to simplify it. + // Presently, this is only an issue for quantifiers, which can have a value + // but don't show up in our substitution map above. + n = m->getValue(n); + Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl; + // The result should be == true. if(n != NodeManager::currentNM()->mkConst(true)) { Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index ade9ffc26..9b4f24566 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -285,7 +285,7 @@ struct TupleSelectTypeRule { const TupleSelect& ts = n.getOperator().getConst<TupleSelect>(); TypeNode tupleType = n[0].getType(check); if(!tupleType.isTuple()) { - if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) { + if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) { throw TypeCheckingExceptionPrivate(n, "Tuple-select expression formed over non-tuple"); } tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); @@ -309,7 +309,7 @@ struct TupleUpdateTypeRule { TypeNode newValue = n[1].getType(check); if(check) { if(!tupleType.isTuple()) { - if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) { + if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) { throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); } tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 8ee275f70..2a74f6d15 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -92,23 +92,21 @@ public: newEnumerators(); } - DatatypesEnumerator(const DatatypesEnumerator& other) : - TypeEnumeratorBase<DatatypesEnumerator>(other.getType()), - d_datatype(other.d_datatype), - d_ctor(other.d_ctor), - d_zeroCtor(other.d_zeroCtor), + DatatypesEnumerator(const DatatypesEnumerator& de) throw() : + TypeEnumeratorBase<DatatypesEnumerator>(de.getType()), + d_datatype(de.d_datatype), + d_ctor(de.d_ctor), + d_zeroCtor(de.d_zeroCtor), d_argEnumerators(NULL) { - - if (other.d_argEnumerators != NULL) { - d_argEnumerators = new TypeEnumerator*[d_datatype[d_ctor].getNumArgs()]; + + if(de.d_argEnumerators != NULL) { + newEnumerators(); for(size_t a = 0; a < d_datatype[d_ctor].getNumArgs(); ++a) { - if (other.d_argEnumerators[a] != NULL) { - d_argEnumerators[a] = new TypeEnumerator(*other.d_argEnumerators[a]); - } else { - d_argEnumerators[a] = NULL; + if(de.d_argEnumerators[a] != NULL) { + d_argEnumerators[a] = new TypeEnumerator(*de.d_argEnumerators[a]); } - } - } + } + } } ~DatatypesEnumerator() throw() { @@ -174,6 +172,14 @@ public: class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { TypeEnumerator** d_enumerators; + /** Allocate and initialize the delegate enumerators */ + void newEnumerators() { + d_enumerators = new TypeEnumerator*[getType().getNumChildren()]; + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + d_enumerators[i] = NULL; + } + } + void deleteEnumerators() throw() { if(d_enumerators != NULL) { for(size_t i = 0; i < getType().getNumChildren(); ++i) { @@ -189,9 +195,20 @@ public: TupleEnumerator(TypeNode type) throw() : TypeEnumeratorBase<TupleEnumerator>(type) { Assert(type.isTuple()); - d_enumerators = new TypeEnumerator*[type.getNumChildren()]; - for(size_t i = 0; i < type.getNumChildren(); ++i) { - d_enumerators[i] = new TypeEnumerator(type[i]); + newEnumerators(); + } + + TupleEnumerator(const TupleEnumerator& te) throw() : + TypeEnumeratorBase<TupleEnumerator>(te.getType()), + d_enumerators(NULL) { + + if(te.d_enumerators != NULL) { + newEnumerators(); + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + if(te.d_enumerators[i] != NULL) { + d_enumerators[i] = new TypeEnumerator(*te.d_enumerators[i]); + } + } } } @@ -240,9 +257,19 @@ public: class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> { TypeEnumerator** d_enumerators; + /** Allocate and initialize the delegate enumerators */ + void newEnumerators() { + const Record& rec = getType().getConst<Record>(); + d_enumerators = new TypeEnumerator*[rec.getNumFields()]; + for(size_t i = 0; i < rec.getNumFields(); ++i) { + d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second)); + } + } + void deleteEnumerators() throw() { if(d_enumerators != NULL) { - for(size_t i = 0; i < getType().getNumChildren(); ++i) { + const Record& rec = getType().getConst<Record>(); + for(size_t i = 0; i < rec.getNumFields(); ++i) { delete d_enumerators[i]; } delete [] d_enumerators; @@ -255,12 +282,20 @@ public: RecordEnumerator(TypeNode type) throw() : TypeEnumeratorBase<RecordEnumerator>(type) { Assert(type.isRecord()); - const Record& rec = getType().getConst<Record>(); - Debug("te") << "creating record enumerator for " << type << std::endl; - d_enumerators = new TypeEnumerator*[rec.getNumFields()]; - for(size_t i = 0; i < rec.getNumFields(); ++i) { - Debug("te") << " - sub-enumerator for " << rec[i].second << std::endl; - d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second)); + newEnumerators(); + } + + RecordEnumerator(const RecordEnumerator& re) throw() : + TypeEnumeratorBase<RecordEnumerator>(re.getType()), + d_enumerators(NULL) { + + if(re.d_enumerators != NULL) { + newEnumerators(); + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + if(re.d_enumerators[i] != NULL) { + d_enumerators[i] = new TypeEnumerator(*re.d_enumerators[i]); + } + } } } diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index d1dbae90c..be6dd5b08 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -92,12 +92,14 @@ Node TheoryQuantifiers::getValue(TNode n) { } } -void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){ - if( fullModel ){ +void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { + if(fullModel) { for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { if((*i).assertion.getKind() == kind::NOT) { + Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl; m->assertPredicate((*i).assertion[0], false); } else { + Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; m->assertPredicate(*i, true); } } diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 0cc64e403..8858cc34b 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -27,12 +27,11 @@ struct substitution_stack_element { bool children_added; substitution_stack_element(TNode node) : node(node), children_added(false) {} -}; - +};/* struct substitution_stack_element */ Node SubstitutionMap::internalSubstitute(TNode t) { - Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << std::endl; + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl; if (d_substitutions.empty()) { return t; @@ -48,7 +47,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) { substitution_stack_element& stackHead = toVisit.back(); TNode current = stackHead.node; - Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << std::endl; + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl; // If node already in the cache we're done, pop from the stack NodeCache::iterator find = d_substitutionCache.find(current); @@ -57,6 +56,14 @@ Node SubstitutionMap::internalSubstitute(TNode t) { continue; } + if (!d_substituteUnderQuantifiers && + (current.getKind() == kind::FORALL || current.getKind() == kind::EXISTS)) { + Debug("substitution::internal") << "--not substituting under quantifier" << endl; + d_substitutionCache[current] = current; + toVisit.pop_back(); + continue; + } + NodeMap::iterator find2 = d_substitutions.find(current); if (find2 != d_substitutions.end()) { Node rhs = (*find2).second; @@ -98,7 +105,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) { } } } - Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl; + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl; d_substitutionCache[current] = result; toVisit.pop_back(); } else { @@ -123,7 +130,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) { } } else { // No children, so we're done - Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << std::endl; + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl; d_substitutionCache[current] = current; toVisit.pop_back(); } @@ -132,7 +139,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) { // Return the substituted version return d_substitutionCache[t]; -} +}/* SubstitutionMap::internalSubstitute() */ /* @@ -258,7 +265,7 @@ void SubstitutionMap::processWorklist(vector<pair<Node, Node> >& equalities, boo void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { - Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl; + Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl; Assert(d_substitutions.find(x) == d_substitutions.end()); // this causes a later assert-fail (the rhs != current one, above) anyway @@ -280,32 +287,32 @@ static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) { SubstitutionMap::NodeMap::const_iterator it = substitutions.begin(); SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end(); - Debug("substitution") << "checking " << node << std::endl; + Debug("substitution") << "checking " << node << endl; for (; it != it_end; ++ it) { - Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << std::endl; + Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << endl; if (node.hasSubterm((*it).first)) { - Debug("substitution") << "-- FAIL" << std::endl; + Debug("substitution") << "-- FAIL" << endl; return false; } } - Debug("substitution") << "-- SUCCEED" << std::endl; + Debug("substitution") << "-- SUCCEED" << endl; return true; } Node SubstitutionMap::apply(TNode t) { - Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << std::endl; + Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl; // Setup the cache if (d_cacheInvalidated) { d_substitutionCache.clear(); d_cacheInvalidated = false; - Debug("substitution") << "-- reset the cache" << std::endl; + Debug("substitution") << "-- reset the cache" << endl; } // Perform the substitution Node result = internalSubstitute(t); - Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl; + Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl; // Assert(check(result, d_substitutions)); diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 31a6b9141..a199256e7 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -62,6 +62,9 @@ private: /** Cache of the already performed substitutions */ NodeCache d_substitutionCache; + /** Whether or not to substitute under quantifiers */ + bool d_substituteUnderQuantifiers; + /** Has the cache been invalidated? */ bool d_cacheInvalidated; @@ -95,10 +98,11 @@ private: public: - SubstitutionMap(context::Context* context) : + SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true) : d_context(context), d_substitutions(context), d_substitutionCache(), + d_substituteUnderQuantifiers(substituteUnderQuantifiers), d_cacheInvalidated(false), d_cacheInvalidator(context, d_cacheInvalidated) { } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index b81bcf799..cc385327e 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -150,7 +150,8 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ - bug216.smt2.expect + bug216.smt2.expect \ + bug484.smt2 if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2 new file mode 100644 index 000000000..afbd72420 --- /dev/null +++ b/test/regress/regress0/bug484.smt2 @@ -0,0 +1,111 @@ +; Preamble -------------- +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort A 0) +(declare-sort B 0) +(declare-sort C 0) +(declare-sort D 0) +(declare-datatypes () ((E (one) (two) (three)))) +(declare-datatypes () ((F (four) (five) (six)))) +(declare-datatypes () ((G (c_G (seven BOOL))))) + +(declare-datatypes () + ((H + (c_H + (foo1 BOOL) + (foo2 A) + (foo3 B) + (foo4 B) + (foo5 Int) + ) + )) +) + +(declare-datatypes () + ((I + (c_I + (bar1 E) + (bar2 Int) + (bar3 Int) + (bar4 A) + ) + )) +) + +(declare-datatypes () + ((J + (c_J + (f1 BOOL) + (f2 Int) + (f3 Int) + (f4 Int) + (f5 I) + (f6 B) + (f7 C) + ) + )) +) + +(declare-datatypes () + ((K + (c_K + (g1 BOOL) + (g2 F) + (g3 A) + (g4 BOOL) + ) + )) +) + +; Var Decls -------------- +(declare-fun s1 () (Array A J)) +(declare-fun s2 () (Array A J)) +(declare-fun e1 () (Array A K)) +(declare-fun e2 () (Array A K)) +(declare-fun x () A) +(declare-fun y () A) +(declare-fun foo (A) A) +(declare-fun bar (A) C) + + +; Asserts -------------- +(assert + (not + (= + (ite + (=> + (= y (g3 (select e1 x))) + (=> + (= s2 + (store + s1 + y + (let ((z (select s1 y))) + (c_J + (f1 z) + (f2 z) + (- (f3 (select s1 y)) 1) + (f4 z) + (f5 z) + (f6 z) + (f7 z) + ) + ) + ) + ) + (forall ((s A)) (= (g3 (select e2 s)) s)) + ) + ) + Truth + Falsity + ) + Truth + ) + ) +) + +(check-sat) |