diff options
-rw-r--r-- | src/options/options_template.cpp | 6 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 7 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 31 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 33 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 7 | ||||
-rw-r--r-- | src/smt/options | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 146 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 8 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 1 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 5 | ||||
-rw-r--r-- | src/theory/model.cpp | 2 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 16 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 26 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.h | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 30 | ||||
-rw-r--r-- | src/util/model.h | 4 | ||||
-rw-r--r-- | src/util/uninterpreted_constant.cpp | 2 |
19 files changed, 265 insertions, 76 deletions
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<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || + tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(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<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || + tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(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; i<tn.getNumChildren()-1; i++ ){ - if( i>0 ) 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<Datatype>().getName(); break; + case kind::UNINTERPRETED_CONSTANT: { + const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>(); + 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<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || + tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(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; i<tn.getNumChildren()-1; i++ ){ - if( i>0 ) 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<DeclareFunctionCommand*>(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 @@ -198,6 +198,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 * and logic for the problem are set (at least, those options that are @@ -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; i<type.getNumChildren()-1; i++ ){ std::stringstream ss; ss << argPrefix << (i+1); - vars.push_back( NodeManager::currentNM()->mkSkolem( 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 */ |