From: Morgan Deters Date: Wed, 12 Sep 2012 20:31:59 +0000 (+0000) Subject: Adding model assertions after SAT responses. X-Git-Tag: cvc5-1.0.0~7815 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dce6be13f8eb90006c7ceb8d43a8a78da23ca838;p=cvc5.git Adding model assertions after SAT responses. To enable, use --check-models. Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not. This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too. By default, --check-models is quiet (no output unless it detects a problem). That allows regression runs to pass unless there are problems: make regress CVC4_REGRESSION_ARGS=--check-models To see it work, use -v in addition to --check-models. There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state. --check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models. This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting). Also: * TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants) * The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2) * The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols) --- diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 2c1323661..ff863bf61 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -260,7 +260,7 @@ void Options::printUsage(const std::string msg, std::ostream& out) { void Options::printShortUsage(const std::string msg, std::ostream& out) { out << msg << mostCommonOptionsDescription << std::endl << optionsFootnote << std::endl - << "For full usage, please use --help." << std::endl << std::flush; + << "For full usage, please use --help." << std::endl << std::endl << std::flush; } void Options::printLanguageHelp(std::ostream& out) { @@ -295,7 +295,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options} { NULL, no_argument, NULL, '\0' } };/* cmdlineOptions */ -#line 292 "${template}" +#line 299 "${template}" static void preemptGetopt(int& argc, char**& argv, const char* opt) { const size_t maxoptlen = 128; @@ -422,7 +422,7 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { switch(c) { ${all_modules_option_handlers} -#line 419 "${template}" +#line 426 "${template}" case ':': // This can be a long or short option, and the way to get at the diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 39d76728a..85742feef 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -152,6 +152,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || @@ -187,7 +188,7 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* AstPrinter::toStream(CommandStatus*) */ void AstPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ - + out << "Model()"; } static void toStream(std::ostream& out, const EmptyCommand* c) throw() { @@ -293,6 +294,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << " >> )"; } +static void toStream(std::ostream& out, const GetModelCommand* c) throw() { + out << "GetModel()"; +} + static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "GetAssignment()"; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 5803ad23f..7f66d6fa0 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -98,7 +98,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo if(types) { // print the whole type, but not *its* type out << ":"; - n.getType().toStream(out, -1, false, language::output::LANG_CVC4); + n.getType().toStream(out, -1, false, false, language::output::LANG_CVC4); } return; } @@ -164,10 +164,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; default: - Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl; - out << n.getKind(); - break; + // fall back on whatever operator<< does on underlying type; we + // might luck out and print something reasonable + kind::metakind::NodeValueConstPrinter::toStream(out, n); } + return; } @@ -213,6 +214,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo case kind::TUPLE: // no-op break; + case kind::LAMBDA: + op << "LAMBDA"; + opType = PREFIX; + break; case kind::APPLY: toStream(op, n.getOperator(), depth, types, true); break; @@ -225,6 +230,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } } break; + // BOOL case kind::AND: op << "AND"; @@ -691,6 +697,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || @@ -768,17 +775,7 @@ void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) }else{ out << tn; } - out << " = "; - if( tn.isFunction() || tn.isPredicate() ){ - out << "LAMBDA ("; - for( size_t i=0; i0 ) out << ", "; - out << "$x" << (i+1) << " : " << tn[i]; - } - out << "): "; - } - out << tm->getValue( n ); - out << ";" << std::endl; + out << " = " << tm->getValue( n ) << ";" << std::endl; /* //for table format (work in progress) @@ -920,6 +917,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << " ))"; } +static void toStream(std::ostream& out, const GetModelCommand* c) throw() { + out << "% (get-model)"; +} + static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "% (get-assignment)"; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9400b7732..8356f9e49 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -177,6 +177,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, out << n.getConst().getName(); break; + case kind::UNINTERPRETED_CONSTANT: { + const UninterpretedConstant& uc = n.getConst(); + out << '@' << uc; + break; + } + default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -480,6 +486,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || @@ -546,21 +553,15 @@ void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type ) } }else if( c_type==Model::COMMAND_DECLARE_FUN ){ Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() ); - TypeNode tn = n.getType(); - out << "(define-fun " << n << " ("; - if( tn.isFunction() || tn.isPredicate() ){ - for( size_t i=0; i0 ) out << " "; - out << "($x" << (i+1) << " " << tn[i] << ")"; - } - out << ") " << tn.getRangeType(); - }else{ - out << ") " << tn; + Node val = tm->getValue( n ); + if(val.getKind() == kind::LAMBDA) { + out << "(define-fun " << n << " " << val[0] + << " " << n.getType().getRangeType() + << " " << val[1] << ")" << std::endl; + } else { + out << "(define-fun " << n << " () " + << n.getType() << " " << val << ")" << std::endl; } - out << " "; - out << tm->getValue( n ); - out << ")" << std::endl; - /* //for table format (work in progress) bool printedModel = false; @@ -713,6 +714,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << " ))"; } +static void toStream(std::ostream& out, const GetModelCommand* c) throw() { + out << "(get-model)"; +} + static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "(get-assignment)"; } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 464a41d74..e550d5ef2 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -110,7 +110,7 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_context = context; if( options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ) { - Notice() << "minisat: Incremental solving is disabled" + Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)" << " unless using internal decision strategy." << std::endl; } @@ -118,12 +118,13 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, options::incrementalSolving() || options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ); - // Setup the verbosity + // Set up the verbosity d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1; - // Setup the random decision parameters + // Set up the random decision parameters d_minisat->random_var_freq = options::satRandomFreq(); d_minisat->random_seed = options::satRandomSeed(); + // Give access to all possible options in the sat solver d_minisat->var_decay = options::satVarDecay(); d_minisat->clause_decay = options::satClauseDecay(); diff --git a/src/smt/options b/src/smt/options index bb0cf1a00..81891acf7 100644 --- a/src/smt/options +++ b/src/smt/options @@ -32,6 +32,8 @@ option doStaticLearning static-learning /--no-static-learning bool :default true common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands +option checkModels check-models --check-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h" + after SAT/INVALID, double-check that the generated model satisfies all user assertions common-option produceAssignments produce-assignments --produce-assignments bool support the get-assignment command option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b9732c32e..ba7973405 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -280,7 +280,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), - d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0) { + d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), + d_checkModelTime("smt::SmtEngine::checkModelTime") { SmtScope smts(this); @@ -295,6 +296,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : StatisticsRegistry::registerStat(&d_cnfConversionTime); StatisticsRegistry::registerStat(&d_numAssertionsPre); StatisticsRegistry::registerStat(&d_numAssertionsPost); + StatisticsRegistry::registerStat(&d_checkModelTime); // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) @@ -355,6 +357,17 @@ void SmtEngine::finalOptionsAreSet() { return; } + if(options::checkModels()) { + if(! options::produceModels()) { + Notice() << "SmtEngine: turning on produce-models to support check-model" << std::endl; + setOption("produce-models", SExpr("true")); + } + if(! options::interactive()) { + Notice() << "SmtEngine: turning on interactive-mode to support check-model" << std::endl; + setOption("interactive-mode", SExpr("true")); + } + } + if(! d_logic.isLocked()) { // ensure that our heuristics are properly set up setLogicInternal(); @@ -430,6 +443,7 @@ SmtEngine::~SmtEngine() throw() { StatisticsRegistry::unregisterStat(&d_cnfConversionTime); StatisticsRegistry::unregisterStat(&d_numAssertionsPre); StatisticsRegistry::unregisterStat(&d_numAssertionsPost); + StatisticsRegistry::unregisterStat(&d_checkModelTime); delete d_private; @@ -819,6 +833,7 @@ void SmtEngine::defineFunction(Expr func, // Permit (check-sat) (define-fun ...) (get-value ...) sequences. // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks // d_haveAdditions = true; + Debug("smt") << "definedFunctions insert " << funcNode << " " << formulaNode << std::endl; d_definedFunctions->insert(funcNode, def); } @@ -1634,8 +1649,13 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) { Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl; + // Check that SAT results generate a model correctly. + if(options::checkModels() && r.asSatisfiabilityResult() == Result::SAT) { + checkModel(); + } + return r; -} +}/* SmtEngine::checkSat() */ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) { @@ -1694,8 +1714,13 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) { Trace("smt") << "SMT query(" << e << ") ==> " << r << endl; + // Check that SAT results generate a model correctly. + if(options::checkModels() && r.asSatisfiabilityResult() == Result::SAT) { + checkModel(); + } + return r; -} +}/* SmtEngine::query() */ Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException) { Assert(e.getExprManager() == d_exprManager); @@ -1877,7 +1902,7 @@ void SmtEngine::addToModelCommand( Command* c, int c_type ){ } } -Model* SmtEngine::getModel() throw(ModalException, AssertionException){ +Model* SmtEngine::getModel() throw(ModalException, AssertionException) { Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); @@ -1888,7 +1913,7 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){ } if(d_status.isNull() || - d_status.asSatisfiabilityResult() == Result::UNSAT || + d_status.asSatisfiabilityResult() == Result::UNSAT || d_problemExtended) { const char* msg = "Cannot get the current model unless immediately " @@ -1903,6 +1928,117 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){ return d_theoryEngine->getModel(); } +void SmtEngine::checkModel() throw(InternalErrorException) { + // --check-model implies --interactive, which enables the assertion list, + // so we should be ok. + Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()"); + + TimerStat::CodeTimer checkModelTimer(d_checkModelTime); + + // Throughout, we use Notice() to give diagnostic output. + // + // If this function is running, the user gave --check-model (or equivalent), + // and if Notice() is on, the user gave --verbose (or equivalent). + + Notice() << "SmtEngine::checkModel(): generating model" << endl; + theory::TheoryModel* m = d_theoryEngine->getModel(); + if(Notice.isOn()) { + printModel(Notice.getStream(), m); + } + + // We have a "fake context" for the substitution map (we don't need it + // to be context-dependent) + context::Context fakeContext; + theory::SubstitutionMap substitutions(&fakeContext); + + for(size_t k = 0; k < m->getNumCommands(); ++k) { + DeclareFunctionCommand* c = dynamic_cast(m->getCommand(k)); + Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl; + if(c == NULL) { + // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ... + Notice() << "SmtEngine::checkModel(): skipping..." << endl; + } else { + // We have a DECLARE-FUN: + // + // We'll first do some checks, then add to our substitution map + // the mapping: function symbol |-> value + + Expr func = c->getFunction(); + Node val = m->getValue(func); + + Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl; + + // (1) check that the value is actually a value + if(!val.isConst()) { + Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl; + stringstream ss; + ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl + << "model value for " << func << endl + << " is " << val << endl + << "and that is not a constant (.isConst() == false)." << endl + << "Run with `--check-models -v' for additional diagnostics."; + InternalError(ss.str()); + } + + // (2) if the value is a lambda, ensure the lambda doesn't contain the + // function symbol (since then the definition is recursive) + if(val.getKind() == kind::LAMBDA) { + // first apply the model substitutions we have so far + Node n = substitutions.apply(val[1]); + // now check if n contains func by doing a substitution + // [func->func2] and checking equality of the Nodes. + // (this just a way to check if func is in n.) + theory::SubstitutionMap subs(&fakeContext); + Node func2 = NodeManager::currentNM()->mkSkolem(TypeNode::fromType(func.getType())); + subs.addSubstitution(func, func2); + if(subs.apply(n) != n) { + Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl; + stringstream ss; + ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl + << "considering model value for " << func << endl + << "body of lambda is: " << val << endl; + if(n != val[1]) { + ss << "body substitutes to: " << n << endl; + } + ss << "so " << func << " is defined in terms of itself." << endl + << "Run with `--check-models -v' for additional diagnostics."; + InternalError(ss.str()); + } + } + + // (3) checks complete, add the substitution + substitutions.addSubstitution(func, val); + } + } + + // Now go through all our user assertions checking if they're satisfied. + for(AssertionList::const_iterator i = d_assertionList->begin(); i != d_assertionList->end(); ++i) { + Notice() << "SmtEngine::checkModel(): checking assertion " << *i << endl; + Node n = Node::fromExpr(*i); + + // Apply our model value substitutions. + n = substitutions.apply(n); + Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl; + + // Simplify the result. + n = Node::fromExpr(simplify(n.toExpr())); + Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; + + // The result should be == true. + if(n != NodeManager::currentNM()->mkConst(true)) { + Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" << endl; + stringstream ss; + ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl + << "assertion: " << *i << endl + << "simplifies to: " << n << endl + << "expected `true'." << endl + << "Run with `--check-models -v' for additional diagnostics."; + InternalError(ss.str()); + } + } + Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; +} + Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2c99bc7eb..5b3229dea 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -197,6 +197,12 @@ class CVC4_PUBLIC SmtEngine { */ smt::SmtEnginePrivate* d_private; + /** + * Check that a generated Model (via getModel()) actually satisfies + * all user assertions. + */ + void checkModel() throw(InternalErrorException); + /** * This is something of an "init" procedure, but is idempotent; call * as often as you like. Should be called whenever the final options @@ -281,6 +287,8 @@ class CVC4_PUBLIC SmtEngine { IntStat d_numAssertionsPre; /** Num of assertions after ite removal */ IntStat d_numAssertionsPost; + /** time spent in checkModel() */ + TimerStat d_checkModelTime; public: diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index c4c3435a2..1218f3809 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -341,6 +341,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule constant SUBTYPE_TYPE \ ::CVC4::Predicate \ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 95ede1c46..7bc1d956d 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -161,6 +161,11 @@ public: TypeNode rangeType = n[1].getType(check); return nodeManager->mkFunctionType(argTypes, rangeType); } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::LAMBDA); + return true; + } };/* class LambdaTypeRule */ class SortProperties { diff --git a/src/theory/model.cpp b/src/theory/model.cpp index ed2d69308..ee61c9345 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -98,7 +98,7 @@ Node TheoryModel::getModelValue( TNode n ){ Trace("model") << "TheoryModel::getModelValue " << n << std::endl; //// special case: prop engine handles boolean vars - //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) { + //if(n.isVar() && n.getType().isBoolean()) { // Trace("model") << "-> Propositional variable." << std::endl; // return d_te->getPropEngine()->getValue( n ); //} diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index b7c9278e1..b5f846735 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -75,7 +75,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) { // Children have been processed, so substitute NodeBuilder<> builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << current.getOperator(); + builder << Node(d_substitutionCache[current.getOperator()]); } for (unsigned i = 0; i < current.getNumChildren(); ++ i) { Assert(d_substitutionCache.find(current[i]) != d_substitutionCache.end()); @@ -105,8 +105,16 @@ Node SubstitutionMap::internalSubstitute(TNode t) { toVisit.pop_back(); } else { // Mark that we have added the children if any - if (current.getNumChildren() > 0) { + if (current.getNumChildren() > 0 || current.getMetaKind() == kind::metakind::PARAMETERIZED) { stackHead.children_added = true; + // We need to add the operator, if any + if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { + TNode opNode = current.getOperator(); + NodeCache::iterator opFind = d_substitutionCache.find(opNode); + if (opFind == d_substitutionCache.end()) { + toVisit.push_back(opNode); + } + } // We need to add the children for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { TNode childNode = *child_it; @@ -255,6 +263,10 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl; Assert(d_substitutions.find(x) == d_substitutions.end()); + // this causes a later assert-fail (the rhs != current one, above) anyway + // putting it here is easier to diagnose + Assert(x != t, "cannot substitute a term for itself"); + d_substitutions[x] = t; // Also invalidate the cache if necessary diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b0a290b7d..c9fb36830 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -85,7 +85,7 @@ TheoryEngine::TheoryEngine(context::Context* context, // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(context, this); - //build model information if applicable + // build model information if applicable d_curr_model = new theory::DefaultModel( context, "DefaultModel", true ); d_curr_model_builder = new theory::TheoryEngineModelBuilder( this ); @@ -105,6 +105,9 @@ TheoryEngine::~TheoryEngine() { } } + delete d_curr_model_builder; + delete d_curr_model; + delete d_quantEngine; StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index a1500e084..9809b948e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -195,31 +195,6 @@ Node TheoryUF::explain(TNode literal) { void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); if( fullModel ){ -#if 1 - std::map< TypeNode, int > type_count; - //must choose proper representatives - // for each equivalence class, specify the constructor as a representative - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - TypeNode tn = eqc.getType(); - if( tn.isSort() ){ - if( type_count.find( tn )==type_count.end() ){ - type_count[tn] = 0; - } - std::stringstream ss; - ss << Expr::setlanguage(options::outputLanguage()); - ss << "$t_" << tn << (type_count[tn]+1); - type_count[tn]++; - Node rep = NodeManager::currentNM()->mkSkolem( ss.str(), tn ); - Trace("mkVar") << "TheoryUF::collectModelInfo: make variable " << rep << " : " << tn << std::endl; - //specify the constant as the representative - m->assertEquality( eqc, rep, true ); - m->assertRepresentative( rep ); - } - ++eqcs_i; - } -#else std::map< TypeNode, TypeEnumerator* > type_enums; //must choose proper representatives // for each equivalence class, specify the constructor as a representative @@ -239,7 +214,6 @@ void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ } ++eqcs_i; } - #endif } } diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index b8110a2aa..8c79f69df 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -268,7 +268,7 @@ Node UfModelTree::getFunctionValue( const char* argPrefix ){ for( size_t i=0; imkSkolem( ss.str(), type[i] ) ); + vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) ); } return getFunctionValue( vars ); } @@ -415,4 +415,4 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; return defaultVal; -} \ No newline at end of file +} diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 61c0714a3..fd346bc3c 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -127,7 +127,11 @@ public: /** getFunctionValue * Returns a representation of this function. */ - Node getFunctionValue( std::vector< Node >& args ){ return d_tree.getFunctionValue( args, 0, Node::null() ); } + Node getFunctionValue( std::vector< Node >& args ){ + Node body = d_tree.getFunctionValue( args, 0, Node::null() ); + Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args); + return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body); + } /** getFunctionValue for args with set prefix */ Node getFunctionValue( const char* argPrefix ); /** update diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 8ba39f372..f70d89b30 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -36,12 +36,27 @@ public: if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } else if(node[0].isConst() && node[1].isConst()) { + // uninterpreted constants are all distinct + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); } if (node[0] > node[1]) { Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]); return RewriteResponse(REWRITE_DONE, newNode); } } + if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) { + // resolve away the lambda + context::Context fakeContext; + theory::SubstitutionMap substitutions(&fakeContext); + TNode lambda = node.getOperator(); + 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); + } + return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1])); + } return RewriteResponse(REWRITE_DONE, node); } @@ -49,7 +64,22 @@ public: if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } else if(node[0].isConst() && node[1].isConst()) { + // uninterpreted constants are all distinct + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); + } + } + if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) { + // resolve away the lambda + context::Context fakeContext; + theory::SubstitutionMap substitutions(&fakeContext); + TNode lambda = node.getOperator(); + 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); } + return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1])); } return RewriteResponse(REWRITE_DONE, node); } diff --git a/src/util/model.h b/src/util/model.h index 9b7db536f..36a5464b4 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -43,13 +43,15 @@ private: std::vector< Command* > d_commands; std::vector< int > d_command_types; public: + /** virtual destructor */ + virtual ~Model() {} /** add command */ virtual void addCommand( Command* c, int c_type ){ d_commands.push_back( c ); d_command_types.push_back( c_type ); } /** get number of commands to report */ - int getNumCommands() { return (int)d_commands.size(); } + size_t getNumCommands() { return d_commands.size(); } /** get command */ Command* getCommand( int i ) { return d_commands[i]; } /** get type of command */ diff --git a/src/util/uninterpreted_constant.cpp b/src/util/uninterpreted_constant.cpp index 766d86428..37510cce1 100644 --- a/src/util/uninterpreted_constant.cpp +++ b/src/util/uninterpreted_constant.cpp @@ -34,7 +34,7 @@ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { while((i = t.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ1234567890_", i)) != string::npos) { t.replace(i, 1, 1, '_'); } - return out << "_uc_" << t << '_' << uc.getIndex(); + return out << "uc_" << t << '_' << uc.getIndex(); } }/* CVC4 namespace */