summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/options_template.cpp6
-rw-r--r--src/printer/ast/ast_printer.cpp7
-rw-r--r--src/printer/cvc/cvc_printer.cpp31
-rw-r--r--src/printer/smt2/smt2_printer.cpp33
-rw-r--r--src/prop/minisat/minisat.cpp7
-rw-r--r--src/smt/options2
-rw-r--r--src/smt/smt_engine.cpp146
-rw-r--r--src/smt/smt_engine.h8
-rw-r--r--src/theory/builtin/kinds1
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h5
-rw-r--r--src/theory/model.cpp2
-rw-r--r--src/theory/substitutions.cpp16
-rw-r--r--src/theory/theory_engine.cpp5
-rw-r--r--src/theory/uf/theory_uf.cpp26
-rw-r--r--src/theory/uf/theory_uf_model.cpp4
-rw-r--r--src/theory/uf/theory_uf_model.h6
-rw-r--r--src/theory/uf/theory_uf_rewriter.h30
-rw-r--r--src/util/model.h4
-rw-r--r--src/util/uninterpreted_constant.cpp2
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback