From e256e63588a867b9ea82e03cfc684c2ea2ca1738 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 8 Oct 2012 22:51:08 +0000 Subject: [PATCH] * Models' SubstitutionMaps are now attached to the user context (rather than SAT context) * Enable part of CVC3 system test (resolves bug 375) * Fix infinite recursion in beta reduction code (resolves bug 417) * Some model-building assertions have been added * Other minor changes (this commit was certified error- and warning-free by the test-and-commit script.) --- contrib/cut-release | 4 +++ src/parser/cvc/Cvc.g | 18 ++++++---- src/smt/options | 2 +- src/theory/arith/kinds | 3 ++ src/theory/arith/type_enumerator.h | 54 ++++++++++++++++++++++++++++++ src/theory/model.cpp | 1 + src/theory/theory_engine.cpp | 2 +- src/theory/uf/theory_uf_rewriter.h | 18 +++++++++- src/util/hash.h | 7 ++++ test/system/cvc3_main.cpp | 8 ++--- 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 { + Integer d_int; + SubrangeBounds d_bounds; + bool d_direction;// true == +, false == - + +public: + + SubrangeEnumerator(TypeNode type) throw(AssertionException) : + TypeEnumeratorBase(type), + d_int(0), + d_bounds(type.getConst()), + 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 HashU = std::hash > +struct PairHashFunction { + size_t operator()(const std::pair& 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; -- 2.30.2