diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
commit | b122cec27ca27d0b48e786191448e0053be78ed0 (patch) | |
tree | 615981d8623e830894f02fc528b173ac7461f934 /src/smt | |
parent | 3da16da97df7cd2efd4b113db3bfef8b9c138ebe (diff) |
Tuples and records merge. Resolves bug 270.
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 2 | ||||
-rw-r--r-- | src/smt/model_postprocessor.cpp | 52 | ||||
-rw-r--r-- | src/smt/model_postprocessor.h | 50 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 43 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 26 |
5 files changed, 159 insertions, 14 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 5555a6190..82601e3c3 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ smt_engine.h \ + model_postprocessor.cpp \ + model_postprocessor.h \ smt_engine_scope.cpp \ smt_engine_scope.h \ command_list.cpp \ diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp new file mode 100644 index 000000000..38fd3ab8b --- /dev/null +++ b/src/smt/model_postprocessor.cpp @@ -0,0 +1,52 @@ +/********************* */ +/*! \file model_postprocessor.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief + ** + ** + **/ + +#include "smt/model_postprocessor.h" + +using namespace CVC4; +using namespace CVC4::smt; + +void ModelPostprocessor::visit(TNode current, TNode parent) { + Debug("tuprec") << "visiting " << current << std::endl; + Assert(!alreadyVisited(current, TNode::null())); + if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) { + Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); + NodeBuilder<> b(kind::TUPLE); + for(TNode::iterator i = current.begin(); i != current.end(); ++i) { + Assert(alreadyVisited(*i, TNode::null())); + TNode n = d_nodes[*i]; + b << (n.isNull() ? *i : n); + } + d_nodes[current] = b; + Debug("tuprec") << "returning " << d_nodes[current] << std::endl; + } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) { + Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); + NodeBuilder<> b(kind::RECORD); + b << current.getType().getAttribute(expr::DatatypeRecordAttr()); + for(TNode::iterator i = current.begin(); i != current.end(); ++i) { + Assert(alreadyVisited(*i, TNode::null())); + TNode n = d_nodes[*i]; + b << (n.isNull() ? *i : n); + } + d_nodes[current] = b; + Debug("tuprec") << "returning " << d_nodes[current] << std::endl; + } else { + Debug("tuprec") << "returning self" << std::endl; + // rewrite to self + d_nodes[current] = Node::null(); + } +}/* ModelPostprocessor::visit() */ + diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h new file mode 100644 index 000000000..08e6168d9 --- /dev/null +++ b/src/smt/model_postprocessor.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file model_postprocessor.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief + ** + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__MODEL_POSTPROCESSOR_H +#define __CVC4__MODEL_POSTPROCESSOR_H + +#include "expr/node.h" + +namespace CVC4 { +namespace smt { + +class ModelPostprocessor { +public: + typedef Node return_type; + std::hash_map<TNode, Node, TNodeHashFunction> d_nodes; + + bool alreadyVisited(TNode current, TNode parent) { + return d_nodes.find(current) != d_nodes.end(); + } + + void visit(TNode current, TNode parent); + + void start(TNode n) { } + + Node done(TNode n) { + Assert(alreadyVisited(n, TNode::null())); + TNode retval = d_nodes[n]; + return retval.isNull() ? n : retval; + } +};/* class ModelPostprocessor */ + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__MODEL_POSTPROCESSOR_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5ea16f20f..07e3439fc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -40,11 +40,13 @@ #include "smt/modal_exception.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "smt/model_postprocessor.h" #include "theory/theory_engine.h" #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" #include "util/proof.h" #include "util/boolean_simplification.h" +#include "util/node_visitor.h" #include "util/configuration.h" #include "util/exception.h" #include "smt/command_list.h" @@ -366,14 +368,14 @@ public: d_smt.addToModelCommandAndDump(c); } - void nmNotifyNewVar(TNode n) { + void nmNotifyNewVar(TNode n, bool isGlobal) { DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType()); - d_smt.addToModelCommandAndDump(c); + d_smt.addToModelCommandAndDump(c, isGlobal); } - void nmNotifyNewSkolem(TNode n, const std::string& comment) { + void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) { std::string id = n.getAttribute(expr::VarNameAttr()); DeclareFunctionCommand c(id, n.toExpr(), @@ -381,7 +383,7 @@ public: if(Dump.isOn("skolems") && comment != "") { Dump("skolems") << CommentCommand(id + " is " + comment); } - d_smt.addToModelCommandAndDump(c, false, "skolems"); + d_smt.addToModelCommandAndDump(c, isGlobal, false, "skolems"); } Node applySubstitutions(TNode node) const { @@ -502,6 +504,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_definedFunctions(NULL), d_assertionList(NULL), d_assignments(NULL), + d_modelGlobalCommands(), d_modelCommands(NULL), d_dumpCommands(), d_logic(), @@ -2020,7 +2023,6 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, return false; } - void SmtEnginePrivate::processAssertions() { Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); @@ -2389,6 +2391,9 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Add the formula d_problemExtended = true; + if(d_assertionList != NULL) { + d_assertionList->push_back(e.notExpr()); + } d_private->addFormula(e.getNode().notNode()); // Run the check @@ -2440,6 +2445,12 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log return quickCheck().asValidityResult(); } +Node SmtEngine::postprocess(TNode node) { + ModelPostprocessor mpost; + NodeVisitor<ModelPostprocessor> visitor; + return visitor.run(mpost, node); +} + Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); @@ -2458,7 +2469,9 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep // Make sure all preprocessing is done d_private->processAssertions(); - return d_private->simplify(Node::fromExpr(e)).toExpr(); + Node n = d_private->simplify(Node::fromExpr(e)); + n = postprocess(n); + return n.toExpr(); } Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException) { @@ -2478,7 +2491,9 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L Dump("benchmark") << ExpandDefinitionsCommand(e); } hash_map<Node, Node, NodeHashFunction> cache; - return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr(); + Node n = d_private->expandDefinitions(Node::fromExpr(e), cache); + n = postprocess(n); + return n.toExpr(); } Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) { @@ -2520,10 +2535,12 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) { Trace("smt") << "--- getting value of " << n << endl; TheoryModel* m = d_theoryEngine->getModel(); Node resultNode; - if( m ){ - resultNode = m->getValue( n ); + if(m != NULL) { + resultNode = m->getValue(n); } Trace("smt") << "--- got value " << n << " = " << resultNode << endl; + resultNode = postprocess(resultNode); + Trace("smt") << "--- model-post returned " << resultNode << endl; // type-check the result we got Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType())); @@ -2630,7 +2647,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { return SExpr(sexprs); } -void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, const char* dumpTag) { +void SmtEngine::addToModelCommandAndDump(const Command& c, bool isGlobal, bool userVisible, const char* dumpTag) { Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl; SmtScope smts(this); // If we aren't yet fully inited, the user might still turn on @@ -2643,7 +2660,11 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, con // and expects to find their cardinalities in the model. if(/* userVisible && */ (!d_fullyInited || options::produceModels())) { doPendingPops(); - d_modelCommands->push_back(c.clone()); + if(isGlobal) { + d_modelGlobalCommands.push_back(c.clone()); + } else { + d_modelCommands->push_back(c.clone()); + } } if(Dump.isOn(dumpTag)) { if(d_fullyInited) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2590bc8e2..b6fb156f6 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -87,6 +87,10 @@ namespace smt { typedef context::CDList<Command*, CommandCleanup> CommandList; }/* CVC4::smt namespace */ +namespace theory { + class TheoryModel; +}/* CVC4::theory namespace */ + namespace stats { StatisticsRegistry* getStatisticsRegistry(SmtEngine*); }/* CVC4::stats namespace */ @@ -144,8 +148,16 @@ class CVC4_PUBLIC SmtEngine { AssignmentSet* d_assignments; /** - * A list of commands that should be in the Model. Only maintained - * if produce-models option is on. + * A list of commands that should be in the Model globally (i.e., + * regardless of push/pop). Only maintained if produce-models option + * is on. + */ + std::vector<Command*> d_modelGlobalCommands; + + /** + * A list of commands that should be in the Model locally (i.e., + * it is context-dependent on push/pop). Only maintained if + * produce-models option is on. */ smt::CommandList* d_modelCommands; @@ -232,6 +244,13 @@ class CVC4_PUBLIC SmtEngine { void checkModel(bool hardFailure = true); /** + * Postprocess a value for output to the user. Involves doing things + * like turning datatypes back into tuples, length-1-bitvectors back + * into booleans, etc. + */ + Node postprocess(TNode n); + + /** * 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 @@ -293,6 +312,7 @@ class CVC4_PUBLIC SmtEngine { friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); // to access d_modelCommands friend class ::CVC4::Model; + friend class ::CVC4::theory::TheoryModel; // to access getModel(), which is private (for now) friend class GetModelCommand; @@ -304,7 +324,7 @@ class CVC4_PUBLIC SmtEngine { * Add to Model command. This is used for recording a command * that should be reported during a get-model call. */ - void addToModelCommandAndDump(const Command& c, bool userVisible = true, const char* dumpTag = "declarations"); + void addToModelCommandAndDump(const Command& c, bool isGlobal = false, bool userVisible = true, const char* dumpTag = "declarations"); /** * Get the model (only if immediately preceded by a SAT |