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
| 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()); }
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
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"
};/* 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 */
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;
}
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);
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]));
}
}
};/* 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 */
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;
projects / cvc5.git / commitdiff