summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xcontrib/cut-release4
-rw-r--r--src/parser/cvc/Cvc.g18
-rw-r--r--src/smt/options2
-rw-r--r--src/theory/arith/kinds3
-rw-r--r--src/theory/arith/type_enumerator.h54
-rw-r--r--src/theory/model.cpp1
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/uf/theory_uf_rewriter.h18
-rw-r--r--src/util/hash.h7
-rw-r--r--test/system/cvc3_main.cpp8
10 files changed, 103 insertions, 14 deletions
diff --git a/contrib/cut-release b/contrib/cut-release
index 97bc31bb1..0870b6ce0 100755
--- a/contrib/cut-release
+++ b/contrib/cut-release
@@ -246,5 +246,9 @@ else
echo "You can still make a branch manually, of course."
fi
+echo
+echo "Done. Next steps are to upload and advertise these packages and to add"
+echo "a $version release to Bugzilla."
+
trap '' EXIT
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index b496aa91c..22459037d 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -619,18 +619,22 @@ mainCommand[CVC4::Command*& cmd]
| QUERY_TOK formula[f] { cmd = new QueryCommand(f); }
| CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); }
- | CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
+ | CHECKSAT_TOK { cmd = new CheckSatCommand(); }
/* options */
| OPTION_TOK
( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
- symbolicExpr[sexpr]
- { if(s == "logic") {
- cmd = new SetBenchmarkLogicCommand(sexpr.getValue());
- } else {
- cmd = new SetOptionCommand(s, sexpr);
+ ( symbolicExpr[sexpr]
+ { if(s == "logic") {
+ cmd = new SetBenchmarkLogicCommand(sexpr.getValue());
+ } else {
+ cmd = new SetOptionCommand(s, sexpr);
+ }
}
- }
+ | TRUE_TOK { cmd = new SetOptionCommand(s, SExpr("true")); }
+ | FALSE_TOK { cmd = new SetOptionCommand(s, SExpr("false")); }
+ | { cmd = new SetOptionCommand(s, SExpr("true")); }
+ )
/* push / pop */
| PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); }
diff --git a/src/smt/options b/src/smt/options
index 5be462195..ab5f9330a 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -23,7 +23,7 @@ option expandDefinitions expand-definitions bool :default false
common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
support the get-value and get-model commands
option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- after SAT/INVALID, double-check that the generated model satisfies all user assertions
+ after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
turn on proof generation
# this is just a placeholder for later; it doesn't show up in command-line options listings
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 549e9f19b..a724124bd 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -61,6 +61,9 @@ enumerator REAL_TYPE \
enumerator INTEGER_TYPE \
"::CVC4::theory::arith::IntegerEnumerator" \
"theory/arith/type_enumerator.h"
+enumerator SUBRANGE_TYPE \
+ "::CVC4::theory::arith::SubrangeEnumerator" \
+ "theory/arith/type_enumerator.h"
operator LT 2 "less than, x < y"
operator LEQ 2 "less than or equal, x <= y"
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 4dd139be7..8b30a4ddf 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -110,6 +110,60 @@ public:
};/* class IntegerEnumerator */
+class SubrangeEnumerator : public TypeEnumeratorBase<SubrangeEnumerator> {
+ Integer d_int;
+ SubrangeBounds d_bounds;
+ bool d_direction;// true == +, false == -
+
+public:
+
+ SubrangeEnumerator(TypeNode type) throw(AssertionException) :
+ TypeEnumeratorBase<SubrangeEnumerator>(type),
+ d_int(0),
+ d_bounds(type.getConst<SubrangeBounds>()),
+ d_direction(d_bounds.lower.hasBound()) {
+
+ d_int = d_direction ? d_bounds.lower.getBound() : d_bounds.upper.getBound();
+
+ Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+ // if we're counting down, there's no lower bound
+ Assert(d_direction || !d_bounds.lower.hasBound());
+ }
+
+ Node operator*() throw() {
+ if(isFinished()) {
+ throw NoMoreValuesException(getType());
+ }
+ return NodeManager::currentNM()->mkConst(Rational(d_int));
+ }
+
+ SubrangeEnumerator& operator++() throw() {
+ if(d_direction) {
+ if(!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound()) {
+ d_int += 1;
+ }
+ } else {
+ // if we're counting down, there's no lower bound
+ d_int -= 1;
+ }
+ // sequence is 0, 1, -1, 2, -2, 3, -3, ...
+ if(d_int <= 0) {
+ d_int = -d_int + 1;
+ } else {
+ d_int = -d_int;
+ }
+ return *this;
+ }
+
+ bool isFinished() throw() {
+ // if we're counting down, there's no lower bound
+ return d_direction &&
+ (!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound());
+ }
+
+};/* class SubrangeEnumerator */
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index d97781ab7..82d602017 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -514,6 +514,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
Node n;
for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
n = typeConstSet.nextTypeEnum(t);
+ Assert(!n.isNull(), "out of values for finite type enumeration while building model");
constantReps[*i] = n;
Trace("model-builder") << " New Const: Setting constant rep of " << (*i) << " to " << n << endl;
}
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 252109a26..08073c147 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -91,7 +91,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_quantEngine = new QuantifiersEngine(context, this);
// build model information if applicable
- d_curr_model = new theory::TheoryModel( context, "DefaultModel", true );
+ d_curr_model = new theory::TheoryModel( userContext, "DefaultModel", true );
d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
StatisticsRegistry::registerStat(&d_combineTheoriesTime);
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index f70d89b30..50211f1ad 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -77,7 +77,23 @@ public:
for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) {
// typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc.
Assert(formal != node.end());
- substitutions.addSubstitution(*formal, *arg);
+ // This rewrite step is important: if we have (f (f 5)) for
+ // some lambda term f, we want to beta-reduce the inside (f 5)
+ // application first. Otherwise, we can end up in infinite
+ // recursion, because f's formal (say "x") gives the
+ // substitution "x |-> (f 5)". Fine, the body of the lambda
+ // gets (f 5) in place for x. But since the same lambda ("f")
+ // now occurs in the body, it's got the same bound var "x", so
+ // substitution continues and we replace that x by (f 5). And
+ // then again. :-(
+ //
+ // We need a better solution for distinguishing bound
+ // variables like this, but for now, handle it by going
+ // inside-out. (Quantifiers shouldn't ever have this problem,
+ // so long as the bound vars in different quantifiers are kept
+ // different.)
+ Node n = Rewriter::rewrite(*arg);
+ substitutions.addSubstitution(*formal, n);
}
return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1]));
}
diff --git a/src/util/hash.h b/src/util/hash.h
index 2420b7acd..1d360783a 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -54,6 +54,13 @@ struct StringHashFunction {
}
};/* struct StringHashFunction */
+template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> >
+struct PairHashFunction {
+ size_t operator()(const std::pair<T, U>& pr) const {
+ return HashT()(pr.first) ^ HashU()(pr.second);
+ }
+};/* struct PairHashFunction */
+
}/* CVC4 namespace */
#endif /* __CVC4__HASH_H */
diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp
index a428f605d..13f5e153c 100644
--- a/test/system/cvc3_main.cpp
+++ b/test/system/cvc3_main.cpp
@@ -2140,10 +2140,10 @@ int main(int argc, char** argv)
test3();
cout << "\n}\n\ntest4(): {" << endl;
test4();
- //if (regressLevel > 0) {
- // cout << "\n}\n\ntest5(): {" << endl;
- // test5();
- //}
+ if (regressLevel > 0) {
+ cout << "\n}\n\ntest5(): {" << endl;
+ test5();
+ }
//cout << "\n}\n\ntest6(): {" << endl;
//test6();
cout << "\n}\n\ntest7(): {" << endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback