summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am6
-rw-r--r--src/expr/expr_template.h17
-rw-r--r--src/expr/options4
-rw-r--r--src/expr/options_handlers.h3
-rw-r--r--src/smt/smt_engine.cpp7
-rw-r--r--src/theory/datatypes/theory_datatypes_type_rules.h4
-rw-r--r--src/theory/datatypes/type_enumerator.h83
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp6
-rw-r--r--src/theory/substitutions.cpp37
-rw-r--r--src/theory/substitutions.h6
-rw-r--r--test/regress/regress0/Makefile.am3
-rw-r--r--test/regress/regress0/bug484.smt2111
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback