summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/boolean_terms.cpp1
-rw-r--r--src/smt/model_postprocessor.cpp9
-rw-r--r--src/smt/options20
-rw-r--r--src/smt/options_handlers.h17
-rw-r--r--src/smt/simplification_mode.cpp3
-rw-r--r--src/smt/simplification_mode.h2
-rw-r--r--src/smt/smt_engine.cpp781
-rw-r--r--src/smt/smt_engine.h63
-rw-r--r--src/smt/smt_engine_scope.h7
9 files changed, 574 insertions, 329 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 7744f64ca..29caa92b3 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -726,6 +726,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
goto next_worklist;
}
switch(k) {
+ case kind::INST_ATTRIBUTE:
case kind::BOUND_VAR_LIST:
result.top() << top;
worklist.pop();
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 7c2742ce4..db0ce3487 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -27,15 +27,6 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
// good to go, we have the right type
return n;
}
- if(n.getKind() == kind::LAMBDA) {
- Assert(asType.isFunction());
- Node rhs = rewriteAs(n[1], asType[1]);
- Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs);
- Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl;
- Debug("boolean-terms") << "need type " << asType << endl;
- Assert(out.getType() == asType);
- return out;
- }
if(!n.isConst()) {
// we don't handle non-const right now
return n;
diff --git a/src/smt/options b/src/smt/options
index 9c7eea12f..0dc416474 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -25,7 +25,7 @@ option expandDefinitions expand-definitions bool :default false
always expand symbol definitions in output
common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
support the get-value and get-model commands
-option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
option dumpModels --dump-models bool :default false :link --produce-models
output models after every SAT/INVALID/UNKNOWN response
@@ -37,16 +37,18 @@ option dumpProofs --dump-proofs bool :default false :link --proof
output proofs after every UNSAT/VALID response
option dumpInstantiations --dump-instantiations bool :default false
output instantiations of quantified formulas after every UNSAT/VALID response
-# this is just a placeholder for later; it doesn't show up in command-line options listings
-undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- turn on unsat core generation (NOT YET SUPPORTED)
+option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ turn on unsat core generation
+option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ output unsat cores after every UNSAT/VALID response
+
option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
support the get-assignment command
-# This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
-# is a mode in which the assertion list must be kept. So it belongs here.
-common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
- force interactive mode
+undocumented-option interactiveMode interactive-mode bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
+ deprecated name for produce-assertions
+common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
+ keep an assertions list (enables get-assertions command)
option doITESimp --ite-simp bool :read-write
turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
@@ -91,7 +93,7 @@ common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long
enable time limiting per query (give milliseconds)
common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
enable resource limiting (currently, roughly the number of SAT conflicts)
-common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
+common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long"
enable resource limiting per query
expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 61e17801d..d02b88fd2 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -153,10 +153,6 @@ batch (default) \n\
(MiniSat) propagation for all of them only after reaching a querying command\n\
(CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
\n\
-incremental\n\
-+ run nonclausal simplification and clausal propagation at each ASSERT\n\
- (and at CHECKSAT/QUERY/SUBTYPE)\n\
-\n\
none\n\
+ do not perform nonclausal simplification\n\
";
@@ -283,8 +279,6 @@ inline LogicInfo stringToLogicInfo(std::string option, std::string optarg, SmtEn
inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "batch") {
return SIMPLIFICATION_MODE_BATCH;
- } else if(optarg == "incremental") {
- return SIMPLIFICATION_MODE_INCREMENTAL;
} else if(optarg == "none") {
return SIMPLIFICATION_MODE_NONE;
} else if(optarg == "help") {
@@ -305,6 +299,11 @@ inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(M
}
}
+inline void setProduceAssertions(std::string option, bool value, SmtEngine* smt) throw() {
+ options::produceAssertions.set(value);
+ options::interactiveMode.set(value);
+}
+
// ensure we are a proof-enabled build of CVC4
inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
#ifndef CVC4_PROOF
@@ -316,12 +315,6 @@ inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) th
#endif /* CVC4_PROOF */
}
-inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
- if(value) {
- throw UnrecognizedOptionException("CVC4 does not yet have support for unsatisfiable cores");
- }
-}
-
// This macro is used for setting :regular-output-channel and :diagnostic-output-channel
// to redirect a stream. It maintains all attributes set on the stream.
#define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
diff --git a/src/smt/simplification_mode.cpp b/src/smt/simplification_mode.cpp
index f728fa862..be46badfc 100644
--- a/src/smt/simplification_mode.cpp
+++ b/src/smt/simplification_mode.cpp
@@ -21,9 +21,6 @@ namespace CVC4 {
std::ostream& operator<<(std::ostream& out, SimplificationMode mode) {
switch(mode) {
- case SIMPLIFICATION_MODE_INCREMENTAL:
- out << "SIMPLIFICATION_MODE_INCREMENTAL";
- break;
case SIMPLIFICATION_MODE_BATCH:
out << "SIMPLIFICATION_MODE_BATCH";
break;
diff --git a/src/smt/simplification_mode.h b/src/smt/simplification_mode.h
index 2242e8bdf..b0b78d318 100644
--- a/src/smt/simplification_mode.h
+++ b/src/smt/simplification_mode.h
@@ -26,8 +26,6 @@ namespace CVC4 {
/** Enumeration of simplification modes (when to simplify). */
typedef enum {
- /** Simplify the assertions as they come in */
- SIMPLIFICATION_MODE_INCREMENTAL,
/** Simplify the assertions all together once a check is requested */
SIMPLIFICATION_MODE_BATCH,
/** Don't do simplification */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ea52f43a7..c59d87d40 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -37,6 +37,7 @@
#include "expr/node_builder.h"
#include "expr/node.h"
#include "expr/node_self_iterator.h"
+#include "expr/attribute.h"
#include "prop/prop_engine.h"
#include "proof/theory_proof.h"
#include "smt/modal_exception.h"
@@ -48,6 +49,7 @@
#include "theory/bv/theory_bv_rewriter.h"
#include "proof/proof_manager.h"
#include "main/options.h"
+#include "util/unsat_core.h"
#include "util/proof.h"
#include "proof/proof.h"
#include "proof/proof_manager.h"
@@ -81,6 +83,7 @@
#include "util/sort_inference.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/macros.h"
+#include "theory/quantifiers/fun_def_process.h"
#include "theory/quantifiers/first_order_reasoning.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/options.h"
@@ -137,6 +140,30 @@ public:
Node getFormula() const { return d_formula; }
};/* class DefinedFunction */
+class AssertionPipeline {
+ vector<Node> d_nodes;
+
+public:
+
+ size_t size() const { return d_nodes.size(); }
+
+ void resize(size_t n) { d_nodes.resize(n); }
+ void clear() { d_nodes.clear(); }
+
+ Node& operator[](size_t i) { return d_nodes[i]; }
+ const Node& operator[](size_t i) const { return d_nodes[i]; }
+ void push_back(Node n) { d_nodes.push_back(n); }
+
+ vector<Node>& ref() { return d_nodes; }
+ const vector<Node>& ref() const { return d_nodes; }
+
+ void replace(size_t i, Node n) {
+ PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); );
+ d_nodes[i] = n;
+ }
+
+};/* class AssertionPipeline */
+
struct SmtEngineStatistics {
/** time spent in definition-expansion */
TimerStat d_definitionExpansionTime;
@@ -160,6 +187,8 @@ struct SmtEngineStatistics {
TimerStat d_iteRemovalTime;
/** time spent in theory preprocessing */
TimerStat d_theoryPreprocessTime;
+ /** time spent in theory preprocessing */
+ TimerStat d_rewriteApplyToConstTime;
/** time spent converting to CNF */
TimerStat d_cnfConversionTime;
/** Num of assertions before ite removal */
@@ -192,6 +221,7 @@ struct SmtEngineStatistics {
d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
+ d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
@@ -214,10 +244,12 @@ struct SmtEngineStatistics {
StatisticsRegistry::registerStat(&d_unconstrainedSimpTime);
StatisticsRegistry::registerStat(&d_iteRemovalTime);
StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
+ StatisticsRegistry::registerStat(&d_rewriteApplyToConstTime);
StatisticsRegistry::registerStat(&d_cnfConversionTime);
StatisticsRegistry::registerStat(&d_numAssertionsPre);
StatisticsRegistry::registerStat(&d_numAssertionsPost);
StatisticsRegistry::registerStat(&d_checkModelTime);
+ StatisticsRegistry::registerStat(&d_checkProofTime);
StatisticsRegistry::registerStat(&d_solveTime);
StatisticsRegistry::registerStat(&d_pushPopTime);
StatisticsRegistry::registerStat(&d_processAssertionsTime);
@@ -236,10 +268,12 @@ struct SmtEngineStatistics {
StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime);
StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
+ StatisticsRegistry::unregisterStat(&d_rewriteApplyToConstTime);
StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
StatisticsRegistry::unregisterStat(&d_checkModelTime);
+ StatisticsRegistry::unregisterStat(&d_checkProofTime);
StatisticsRegistry::unregisterStat(&d_solveTime);
StatisticsRegistry::unregisterStat(&d_pushPopTime);
StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
@@ -264,9 +298,6 @@ struct SmtEngineStatistics {
class SmtEnginePrivate : public NodeManagerListener {
SmtEngine& d_smt;
- /** The assertions yet to be preprocessed */
- vector<Node> d_assertionsToPreprocess;
-
/** Learned literals */
vector<Node> d_nonClausalLearnedLiterals;
@@ -281,8 +312,8 @@ class SmtEnginePrivate : public NodeManagerListener {
bool d_propagatorNeedsFinish;
std::vector<Node> d_boolVars;
- /** Assertions to push to sat */
- vector<Node> d_assertionsToCheck;
+ /** Assertions in the preprocessing pipeline */
+ AssertionPipeline d_assertions;
/** Whether any assertions have been processed */
CDO<bool> d_assertionsProcessed;
@@ -319,7 +350,7 @@ class SmtEnginePrivate : public NodeManagerListener {
public:
/**
- * Map from skolem variables to index in d_assertionsToCheck containing
+ * Map from skolem variables to index in d_assertions containing
* corresponding introduced Boolean ite
*/
IteSkolemMap d_iteSkolemMap;
@@ -375,7 +406,7 @@ private:
bool simpITE();
// Simplify based on unconstrained values
- void unconstrainedSimp(std::vector<Node>& assertions);
+ void unconstrainedSimp();
// Ensures the assertions asserted after before now
// effectively come before d_realAssertionsEnd
@@ -386,7 +417,7 @@ private:
* (predicate subtype or integer subrange type) must be constrained
* to be in that type.
*/
- void constrainSubtypes(TNode n, std::vector<Node>& assertions)
+ void constrainSubtypes(TNode n, AssertionPipeline& assertions)
throw();
// trace nodes back to their assertions using CircuitPropagator's BackEdgesMap
@@ -410,13 +441,12 @@ public:
SmtEnginePrivate(SmtEngine& smt) :
d_smt(smt),
- d_assertionsToPreprocess(),
d_nonClausalLearnedLiterals(),
d_realAssertionsEnd(0),
d_booleanTermConverter(NULL),
d_propagator(d_nonClausalLearnedLiterals, true, true),
d_propagatorNeedsFinish(false),
- d_assertionsToCheck(),
+ d_assertions(),
d_assertionsProcessed(smt.d_userContext, false),
d_substitutionsIndex(smt.d_userContext, 0),
d_fakeContext(),
@@ -493,6 +523,10 @@ public:
}
}
+ void nmNotifyDeleteNode(TNode n) {
+ d_smt.d_smtAttributes->deleteAllAttributes(n);
+ }
+
Node applySubstitutions(TNode node) const {
return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
}
@@ -508,9 +542,8 @@ public:
* someone does a push-assert-pop without a check-sat.
*/
void notifyPop() {
- d_assertionsToPreprocess.clear();
+ d_assertions.clear();
d_nonClausalLearnedLiterals.clear();
- d_assertionsToCheck.clear();
d_realAssertionsEnd = 0;
d_iteSkolemMap.clear();
}
@@ -546,7 +579,7 @@ public:
hash_map<Node, Node, NodeHashFunction> cache;
Node n = expandDefinitions(in, cache).toExpr();
// Make sure we've done all preprocessing, etc.
- Assert(d_assertionsToCheck.size() == 0 && d_assertionsToPreprocess.size() == 0);
+ Assert(d_assertions.size() == 0);
return applySubstitutions(n).toExpr();
}
@@ -571,7 +604,9 @@ public:
val = d_smt.d_nodeManager->mkAbstractValue(n.getType());
d_abstractValueMap.addSubstitution(val, n);
}
- return val;
+ // We are supposed to ascribe types to all abstract values that go out.
+ Node retval = d_smt.d_nodeManager->mkNode(kind::APPLY_TYPE_ASCRIPTION, d_smt.d_nodeManager->mkConst(AscriptionType(n.getType().toType())), val);
+ return retval;
}
std::hash_map<Node, Node, NodeHashFunction> rewriteApplyToConstCache;
@@ -627,7 +662,7 @@ public:
}/* namespace CVC4::smt */
SmtEngine::SmtEngine(ExprManager* em) throw() :
- d_context(em->getContext()),
+ d_context(new Context()),
d_userLevels(),
d_userContext(new UserContext()),
d_exprManager(em),
@@ -643,6 +678,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
d_modelCommands(NULL),
d_dumpCommands(),
d_logic(),
+ d_originalOptions(em->getOptions()),
d_pendingPops(0),
d_fullyInited(false),
d_problemExtended(false),
@@ -657,16 +693,16 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
d_cumulativeResourceUsed(0),
d_status(),
d_private(NULL),
+ d_smtAttributes(NULL),
d_statisticsRegistry(NULL),
d_stats(NULL) {
SmtScope smts(this);
+ d_smtAttributes = new expr::attr::SmtAttributes(d_context);
d_private = new smt::SmtEnginePrivate(*this);
d_statisticsRegistry = new StatisticsRegistry();
d_stats = new SmtEngineStatistics();
- PROOF( d_proofManager = new ProofManager(); );
-
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
@@ -689,6 +725,9 @@ void SmtEngine::finishInit() {
// ensure that our heuristics are properly set up
setDefaults();
+ Assert(d_proofManager == NULL);
+ PROOF( d_proofManager = new ProofManager(); );
+
d_decisionEngine = new DecisionEngine(d_context, d_userContext);
d_decisionEngine->init(); // enable appropriate strategies
@@ -702,7 +741,7 @@ void SmtEngine::finishInit() {
// cleanup ordering issue and Nodes/TNodes. If SAT is popped
// first, some user-context-dependent TNodes might still exist
// with rc == 0.
- if(options::interactive() ||
+ if(options::produceAssertions() ||
options::incrementalSolving()) {
// In the case of incremental solving, we appear to need these to
// ensure the relevant Nodes remain live.
@@ -834,8 +873,13 @@ SmtEngine::~SmtEngine() throw() {
delete d_private;
d_private = NULL;
+ delete d_smtAttributes;
+ d_smtAttributes = NULL;
+
delete d_userContext;
d_userContext = NULL;
+ delete d_context;
+ d_context = NULL;
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
@@ -921,9 +965,67 @@ void SmtEngine::setDefaults() {
}
if(options::checkModels()) {
- if(! options::interactive()) {
- Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl;
- setOption("interactive-mode", SExpr("true"));
+ if(! options::produceAssertions()) {
+ Notice() << "SmtEngine: turning on produce-assertions to support check-models" << endl;
+ setOption("produce-assertions", SExpr("true"));
+ }
+ }
+
+ if(options::unsatCores()) {
+ if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
+ if(options::simplificationMode.wasSetByUser()) {
+ throw OptionException("simplification not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off simplification to support unsat-cores" << endl;
+ options::simplificationMode.set(SIMPLIFICATION_MODE_NONE);
+ }
+
+ if(options::unconstrainedSimp()) {
+ if(options::unconstrainedSimp.wasSetByUser()) {
+ throw OptionException("unconstrained simplification not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl;
+ options::unconstrainedSimp.set(false);
+ }
+
+ if(options::pbRewrites()) {
+ if(options::pbRewrites.wasSetByUser()) {
+ throw OptionException("pseudoboolean rewrites not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl;
+ setOption("pb-rewrites", false);
+ }
+
+ if(options::sortInference()) {
+ if(options::sortInference.wasSetByUser()) {
+ throw OptionException("sort inference not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl;
+ options::sortInference.set(false);
+ }
+
+ if(options::preSkolemQuant()) {
+ if(options::preSkolemQuant.wasSetByUser()) {
+ throw OptionException("pre-skolemization not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl;
+ options::preSkolemQuant.set(false);
+ }
+
+ if(options::bitvectorToBool()) {
+ if(options::bitvectorToBool.wasSetByUser()) {
+ throw OptionException("bv-to-bool not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off bitvector-to-bool support unsat-cores" << endl;
+ options::bitvectorToBool.set(false);
+ }
+
+ if(options::bvIntroducePow2()) {
+ if(options::bvIntroducePow2.wasSetByUser()) {
+ throw OptionException("bv-intro-pow2 not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl;
+ setOption("bv-intro-pow2", false);
}
}
@@ -1119,10 +1221,8 @@ void SmtEngine::setDefaults() {
if (options::arithRewriteEq()) {
d_earlyTheoryPP = false;
}
- // Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV
- // and also use it in stop-only mode for QF_AUFLIA, QF_LRA and Quantifiers
- // BUT use neither in ALL_SUPPORTED mode (since it doesn't yet work well
- // with incrementality)
+
+ // Set decision mode based on logic (if not set by user)
if(!options::decisionMode.wasSetByUser()) {
decision::DecisionMode decMode =
// ALL_SUPPORTED
@@ -1215,7 +1315,54 @@ void SmtEngine::setDefaults() {
if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
options::quantConflictFind.set( true );
}
-
+ //for induction techniques
+ if( options::quantInduction() ){
+ if( !options::dtStcInduction.wasSetByUser() ){
+ options::dtStcInduction.set( true );
+ }
+ if( !options::intWfInduction.wasSetByUser() ){
+ options::intWfInduction.set( true );
+ }
+ }
+ if( options::dtStcInduction() ){
+ //leads to unfairness FIXME
+ if( !options::dtForceAssignment.wasSetByUser() ){
+ options::dtForceAssignment.set( true );
+ }
+ }
+ if( options::intWfInduction() ){
+ if( !options::purifyTriggers.wasSetByUser() ){
+ options::purifyTriggers.set( true );
+ }
+ }
+ if( options::conjectureNoFilter() ){
+ if( !options::conjectureFilterActiveTerms.wasSetByUser() ){
+ options::conjectureFilterActiveTerms.set( false );
+ }
+ if( !options::conjectureFilterCanonical.wasSetByUser() ){
+ options::conjectureFilterCanonical.set( false );
+ }
+ if( !options::conjectureFilterModel.wasSetByUser() ){
+ options::conjectureFilterModel.set( false );
+ }
+ }
+ if( options::conjectureGenPerRound.wasSetByUser() ){
+ if( options::conjectureGenPerRound()>0 ){
+ options::conjectureGen.set( true );
+ }else{
+ options::conjectureGen.set( false );
+ }
+ }
+ if( options::fmfFunWellDefined() ){
+ if( !options::finiteModelFind.wasSetByUser() ){
+ options::finiteModelFind.set( true );
+ }
+ }
+ if( options::finiteModelFind() ){
+ if( !options::quantConflictFind.wasSetByUser() ){
+ options::quantConflictFind.set( false );
+ }
+ }
//until bugs 371,431 are fixed
if( ! options::minisatUseElim.wasSetByUser()){
if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){
@@ -1260,17 +1407,10 @@ void SmtEngine::setDefaults() {
}
}
- if (options::incrementalSolving() && options::proof()) {
- Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof" << endl;
+ if(options::incrementalSolving() && (options::proof() || options::unsatCores())) {
+ Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof or --produce-unsat-cores, try --tear-down-incremental instead)" << endl;
setOption("incremental", SExpr("false"));
}
-
- // datatypes theory should assign values to all datatypes terms if logic is quantified
- if (d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
- if( !options::dtForceAssignment.wasSetByUser() ){
- options::dtForceAssignment.set(true);
- }
- }
}
void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
@@ -1323,8 +1463,23 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
} else if(key == "smt-lib-version") {
if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
(value.isRational() && value.getRationalValue() == Rational(2)) ||
- (value.getValue() == "2") ) {
+ value.getValue() == "2" ||
+ value.getValue() == "2.0" ) {
// supported SMT-LIB version
+ if(!options::outputLanguage.wasSetByUser() &&
+ options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) {
+ options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
+ *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_0);
+ }
+ return;
+ } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
+ value.getValue() == "2.5" ) {
+ // supported SMT-LIB version
+ if(!options::outputLanguage.wasSetByUser() &&
+ options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
+ options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
+ *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
+ }
return;
}
Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
@@ -1403,6 +1558,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
throw ModalException("Can't get-info :reason-unknown when the "
"last result wasn't unknown!");
}
+ } else if(key == "assertion-stack-levels") {
+ return SExpr(d_userLevels.size());
} else if(key == "all-options") {
// get the options, like all-statistics
return Options::current().getOptions();
@@ -1636,11 +1793,10 @@ void SmtEnginePrivate::removeITEs() {
Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
// Remove all of the ITE occurrences and normalize
- d_iteRemover.run(d_assertionsToCheck, d_iteSkolemMap);
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]);
+ d_iteRemover.run(d_assertions.ref(), d_iteSkolemMap, true);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
}
-
}
void SmtEnginePrivate::staticLearning() {
@@ -1650,22 +1806,21 @@ void SmtEnginePrivate::staticLearning() {
Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl;
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
NodeBuilder<> learned(kind::AND);
- learned << d_assertionsToCheck[i];
- d_smt.d_theoryEngine->ppStaticLearn(d_assertionsToCheck[i], learned);
+ learned << d_assertions[i];
+ d_smt.d_theoryEngine->ppStaticLearn(d_assertions[i], learned);
if(learned.getNumChildren() == 1) {
learned.clear();
} else {
- d_assertionsToCheck[i] = learned;
+ d_assertions.replace(i, learned);
}
}
}
// do dumping (before/after any preprocessing pass)
-static void dumpAssertions(const char* key,
- const std::vector<Node>& assertionList) {
+static void dumpAssertions(const char* key, const AssertionPipeline& assertionList) {
if( Dump.isOn("assertions") &&
Dump.isOn(string("assertions:") + key) ) {
// Push the simplified assertions to the dump output stream
@@ -1680,8 +1835,11 @@ static void dumpAssertions(const char* key,
bool SmtEnginePrivate::nonClausalSimplify() {
d_smt.finalOptionsAreSet();
- TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
+ if(options::unsatCores()) {
+ return true;
+ }
+ TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
@@ -1694,14 +1852,15 @@ bool SmtEnginePrivate::nonClausalSimplify() {
// Assert all the assertions to the propagator
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "asserting to propagator" << endl;
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- Assert(Rewriter::rewrite(d_assertionsToPreprocess[i]) == d_assertionsToPreprocess[i]);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
// Don't reprocess substitutions
if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) {
continue;
}
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl;
- d_propagator.assertTrue(d_assertionsToPreprocess[i]);
+ Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl;
+ Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl;
+ d_propagator.assertTrue(d_assertions[i]);
}
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -1710,8 +1869,10 @@ bool SmtEnginePrivate::nonClausalSimplify() {
// If in conflict, just return false
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict in non-clausal propagation" << endl;
- d_assertionsToPreprocess.clear();
- d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
+ Assert(!options::unsatCores());
+ d_assertions.clear();
+ d_assertions.push_back(falseNode);
d_propagatorNeedsFinish = true;
return false;
}
@@ -1748,8 +1909,9 @@ bool SmtEnginePrivate::nonClausalSimplify() {
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict with "
<< d_nonClausalLearnedLiterals[i] << endl;
- d_assertionsToPreprocess.clear();
- d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ Assert(!options::unsatCores());
+ d_assertions.clear();
+ d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
d_propagatorNeedsFinish = true;
return false;
}
@@ -1783,8 +1945,9 @@ bool SmtEnginePrivate::nonClausalSimplify() {
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict while solving "
<< learnedLiteral << endl;
- d_assertionsToPreprocess.clear();
- d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ Assert(!options::unsatCores());
+ d_assertions.clear();
+ d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
d_propagatorNeedsFinish = true;
return false;
default:
@@ -1809,8 +1972,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
// constantPropagations.simplifyLHS(t, c, equations, true);
// if (!equations.empty()) {
// Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
- // d_assertionsToPreprocess.clear();
- // d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ // d_assertions.clear();
+ // d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
// return;
// }
// d_topLevelSubstitutions.simplifyRHS(constantPropagations);
@@ -1859,8 +2022,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
hash_set<TNode, TNodeHashFunction> s;
Trace("debugging") << "NonClausal simplify pre-preprocess\n";
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- Node assertion = d_assertionsToPreprocess[i];
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Node assertion = d_assertions[i];
Node assertionNew = newSubstitutions.apply(assertion);
Trace("debugging") << "assertion = " << assertion << endl;
Trace("debugging") << "assertionNew = " << assertionNew << endl;
@@ -1881,17 +2044,16 @@ bool SmtEnginePrivate::nonClausalSimplify() {
}
Trace("debugging") << "\n";
s.insert(assertion);
- d_assertionsToCheck.push_back(assertion);
+ d_assertions.replace(i, assertion);
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "non-clausal preprocessed: "
<< assertion << endl;
}
- d_assertionsToPreprocess.clear();
// If in incremental mode, add substitutions to the list of assertions
if (d_substitutionsIndex > 0) {
NodeBuilder<> substitutionsBuilder(kind::AND);
- substitutionsBuilder << d_assertionsToCheck[d_substitutionsIndex];
+ substitutionsBuilder << d_assertions[d_substitutionsIndex];
pos = newSubstitutions.begin();
for (; pos != newSubstitutions.end(); ++pos) {
// Add back this substitution as an assertion
@@ -1901,8 +2063,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
}
if (substitutionsBuilder.getNumChildren() > 1) {
- d_assertionsToCheck[d_substitutionsIndex] =
- Rewriter::rewrite(Node(substitutionsBuilder));
+ d_assertions.replace(d_substitutionsIndex,
+ Rewriter::rewrite(Node(substitutionsBuilder)));
}
} else {
// If not in incremental mode, must add substitutions to model
@@ -1918,8 +2080,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
}
NodeBuilder<> learnedBuilder(kind::AND);
- Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
- learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1];
+ Assert(d_realAssertionsEnd <= d_assertions.size());
+ learnedBuilder << d_assertions[d_realAssertionsEnd - 1];
for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
Node learned = d_nonClausalLearnedLiterals[i];
@@ -1948,7 +2110,6 @@ bool SmtEnginePrivate::nonClausalSimplify() {
}
d_nonClausalLearnedLiterals.clear();
-
for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
Node cProp = (*pos).first.eqNode((*pos).second);
Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
@@ -1973,8 +2134,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
d_topLevelSubstitutions.addSubstitutions(newSubstitutions);
if(learnedBuilder.getNumChildren() > 1) {
- d_assertionsToCheck[d_realAssertionsEnd - 1] =
- Rewriter::rewrite(Node(learnedBuilder));
+ d_assertions.replace(d_realAssertionsEnd - 1,
+ Rewriter::rewrite(Node(learnedBuilder)));
}
d_propagatorNeedsFinish = true;
@@ -1984,9 +2145,9 @@ bool SmtEnginePrivate::nonClausalSimplify() {
void SmtEnginePrivate::bvAbstraction() {
Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl;
std::vector<Node> new_assertions;
- bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertionsToPreprocess, new_assertions);
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]);
+ bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertions.ref(), new_assertions);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
}
// if we are using the lazy solver and the abstraction
// applies, then UF symbols were introduced
@@ -2001,9 +2162,9 @@ void SmtEnginePrivate::bvAbstraction() {
void SmtEnginePrivate::bvToBool() {
Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
std::vector<Node> new_assertions;
- d_smt.d_theoryEngine->ppBvToBool(d_assertionsToPreprocess, new_assertions);
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]);
+ d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
}
}
@@ -2012,23 +2173,23 @@ bool SmtEnginePrivate::simpITE() {
Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
- unsigned numAssertionOnEntry = d_assertionsToCheck.size();
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
- Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
- d_assertionsToCheck[i] = result;
+ unsigned numAssertionOnEntry = d_assertions.size();
+ for (unsigned i = 0; i < d_assertions.size(); ++i) {
+ Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
+ d_assertions.replace(i, result);
if(result.isConst() && !result.getConst<bool>()){
return false;
}
}
- bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck);
- if(numAssertionOnEntry < d_assertionsToCheck.size()){
+ bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref());
+ if(numAssertionOnEntry < d_assertions.size()){
compressBeforeRealAssertions(numAssertionOnEntry);
}
return result;
}
void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
- size_t curr = d_assertionsToCheck.size();
+ size_t curr = d_assertions.size();
if(before >= curr ||
d_realAssertionsEnd <= 0 ||
d_realAssertionsEnd >= curr){
@@ -2048,24 +2209,24 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
std::vector<Node> intoConjunction;
for(size_t i = before; i<curr; ++i){
- intoConjunction.push_back(d_assertionsToCheck[i]);
+ intoConjunction.push_back(d_assertions[i]);
}
- d_assertionsToCheck.resize(before);
+ d_assertions.resize(before);
size_t lastBeforeItes = d_realAssertionsEnd - 1;
- intoConjunction.push_back(d_assertionsToCheck[lastBeforeItes]);
+ intoConjunction.push_back(d_assertions[lastBeforeItes]);
Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
- d_assertionsToCheck[lastBeforeItes] = newLast;
- Assert(d_assertionsToCheck.size() == before);
+ d_assertions.replace(lastBeforeItes, newLast);
+ Assert(d_assertions.size() == before);
}
-void SmtEnginePrivate::unconstrainedSimp(std::vector<Node>& assertions) {
+void SmtEnginePrivate::unconstrainedSimp() {
TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
- d_smt.d_theoryEngine->ppUnconstrainedSimp(assertions);
+ d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
}
-void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
+void SmtEnginePrivate::constrainSubtypes(TNode top, AssertionPipeline& assertions)
throw() {
Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
@@ -2187,8 +2348,7 @@ size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsi
}
void SmtEnginePrivate::doMiplibTrick() {
- Assert(d_assertionsToPreprocess.empty());
- Assert(d_realAssertionsEnd == d_assertionsToCheck.size());
+ Assert(d_realAssertionsEnd == d_assertions.size());
Assert(!options::incrementalSolving());
const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
@@ -2419,7 +2579,7 @@ void SmtEnginePrivate::doMiplibTrick() {
Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME);
Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
- d_assertionsToCheck.push_back(Rewriter::rewrite(geq.andNode(leq)));
+ d_assertions.push_back(Rewriter::rewrite(geq.andNode(leq)));
SubstitutionMap nullMap(&d_fakeContext);
Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
status = d_smt.d_theoryEngine->solve(geq, nullMap);
@@ -2470,7 +2630,7 @@ void SmtEnginePrivate::doMiplibTrick() {
}
newAssertion = Rewriter::rewrite(newAssertion);
Debug("miplib") << " " << newAssertion << endl;
- d_assertionsToCheck.push_back(newAssertion);
+ d_assertions.push_back(newAssertion);
Debug("miplib") << " assertions to remove: " << endl;
for(vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) {
Debug("miplib") << " " << *k << endl;
@@ -2483,26 +2643,26 @@ void SmtEnginePrivate::doMiplibTrick() {
if(!removeAssertions.empty()) {
Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl;
for(size_t i = 0; i < d_realAssertionsEnd; ++i) {
- if(removeAssertions.find(d_assertionsToCheck[i].getId()) != removeAssertions.end()) {
- Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertionsToCheck[i] << endl;
- d_assertionsToCheck[i] = d_true;
+ if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) {
+ Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl;
+ d_assertions[i] = d_true;
++d_smt.d_stats->d_numMiplibAssertionsRemoved;
- } else if(d_assertionsToCheck[i].getKind() == kind::AND) {
- size_t removals = removeFromConjunction(d_assertionsToCheck[i], removeAssertions);
+ } else if(d_assertions[i].getKind() == kind::AND) {
+ size_t removals = removeFromConjunction(d_assertions[i], removeAssertions);
if(removals > 0) {
- Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertionsToCheck[i] << endl;
+ Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions[i] << endl;
Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals << " conjuncts" << endl;
d_smt.d_stats->d_numMiplibAssertionsRemoved += removals;
}
}
- Debug("miplib") << "had: " << d_assertionsToCheck[i] << endl;
- d_assertionsToCheck[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToCheck[i]));
- Debug("miplib") << "now: " << d_assertionsToCheck[i] << endl;
+ Debug("miplib") << "had: " << d_assertions[i] << endl;
+ d_assertions[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]));
+ Debug("miplib") << "now: " << d_assertions[i] << endl;
}
} else {
Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl;
}
- d_realAssertionsEnd = d_assertionsToCheck.size();
+ d_realAssertionsEnd = d_assertions.size();
}
@@ -2536,7 +2696,7 @@ bool SmtEnginePrivate::simplifyAssertions()
// we add new assertions and need this (in practice, this
// restriction only disables miplib processing during
// re-simplification, which we don't expect to be useful anyway)
- d_realAssertionsEnd == d_assertionsToCheck.size() ) {
+ d_realAssertionsEnd == d_assertions.size() ) {
Chat() << "...fixing miplib encodings..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< "looking for miplib pseudobooleans..." << endl;
@@ -2548,18 +2708,16 @@ bool SmtEnginePrivate::simplifyAssertions()
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;
}
- } else {
- Assert(d_assertionsToCheck.empty());
- d_assertionsToCheck.swap(d_assertionsToPreprocess);
}
- dumpAssertions("post-nonclausal", d_assertionsToCheck);
+ dumpAssertions("post-nonclausal", d_assertions);
Trace("smt") << "POST nonClausalSimplify" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// before ppRewrite check if only core theory for BV theory
- d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertionsToCheck);
+ d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref());
+
+ dumpAssertions("pre-theorypp", d_assertions);
// Theory preprocessing
if (d_smt.d_earlyTheoryPP) {
@@ -2567,17 +2725,16 @@ bool SmtEnginePrivate::simplifyAssertions()
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
// Call the theory preprocessors
d_smt.d_theoryEngine->preprocessStart();
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- Assert(Rewriter::rewrite(d_assertionsToCheck[i]) == d_assertionsToCheck[i]);
- d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
- Assert(Rewriter::rewrite(d_assertionsToCheck[i]) == d_assertionsToCheck[i]);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
+ d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
+ Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
}
}
- dumpAssertions("post-theorypp", d_assertionsToCheck);
+ dumpAssertions("post-theorypp", d_assertions);
Trace("smt") << "POST theoryPP" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// ITE simplification
if(options::doITESimp() &&
@@ -2590,38 +2747,33 @@ bool SmtEnginePrivate::simplifyAssertions()
}
}
- dumpAssertions("post-itesimp", d_assertionsToCheck);
+ dumpAssertions("post-itesimp", d_assertions);
Trace("smt") << "POST iteSimp" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// Unconstrained simplification
if(options::unconstrainedSimp()) {
Chat() << "...doing unconstrained simplification..." << endl;
- unconstrainedSimp(d_assertionsToCheck);
+ unconstrainedSimp();
}
- dumpAssertions("post-unconstrained", d_assertionsToCheck);
+ dumpAssertions("post-unconstrained", d_assertions);
Trace("smt") << "POST unconstrainedSimp" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
Chat() << "...doing another round of nonclausal simplification..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< " doing repeated simplification" << endl;
- d_assertionsToCheck.swap(d_assertionsToPreprocess);
- Assert(d_assertionsToCheck.empty());
bool noConflict = nonClausalSimplify();
if(!noConflict) {
return false;
}
}
- dumpAssertions("post-repeatsimp", d_assertionsToCheck);
+ dumpAssertions("post-repeatsimp", d_assertions);
Trace("smt") << "POST repeatSimp" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
} catch(TypeCheckingExceptionPrivate& tcep) {
// Calls to this function should have already weeded out any
@@ -2807,52 +2959,45 @@ void SmtEnginePrivate::processAssertions() {
Assert(d_smt.d_pendingPops == 0);
// Dump the assertions
- dumpAssertions("pre-everything", d_assertionsToPreprocess);
+ dumpAssertions("pre-everything", d_assertions);
Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- Assert(d_assertionsToCheck.size() == 0);
-
- if (d_assertionsToPreprocess.size() == 0) {
+ if (d_assertions.size() == 0) {
// nothing to do
return;
}
- if (d_assertionsProcessed &&
- ( options::incrementalSolving() ||
- options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL )) {
+ if (d_assertionsProcessed && options::incrementalSolving()) {
// Placeholder for storing substitutions
- d_substitutionsIndex = d_assertionsToPreprocess.size();
- d_assertionsToPreprocess.push_back(NodeManager::currentNM()->mkConst<bool>(true));
+ d_substitutionsIndex = d_assertions.size();
+ d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
}
// Add dummy assertion in last position - to be used as a
// placeholder for any new assertions to get added
- d_assertionsToPreprocess.push_back(NodeManager::currentNM()->mkConst<bool>(true));
+ d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
// any assertions added beyond realAssertionsEnd must NOT affect the
// equisatisfiability
- d_realAssertionsEnd = d_assertionsToPreprocess.size();
+ d_realAssertionsEnd = d_assertions.size();
// Assertions are NOT guaranteed to be rewritten by this point
- dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess);
+ dumpAssertions("pre-definition-expansion", d_assertions);
{
Chat() << "expanding definitions..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
hash_map<Node, Node, NodeHashFunction> cache;
- for(unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- d_assertionsToPreprocess[i] =
- expandDefinitions(d_assertionsToPreprocess[i], cache);
+ for(unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
}
}
- dumpAssertions("post-definition-expansion", d_assertionsToPreprocess);
+ dumpAssertions("post-definition-expansion", d_assertions);
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
!d_smt.d_logic.isPure(THEORY_BV)) {
@@ -2862,146 +3007,157 @@ void SmtEnginePrivate::processAssertions() {
}
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess);
+ d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertions.ref());
}
if ( options::bvAbstraction() &&
!options::incrementalSolving()) {
- dumpAssertions("pre-bv-abstraction", d_assertionsToPreprocess);
+ dumpAssertions("pre-bv-abstraction", d_assertions);
bvAbstraction();
- dumpAssertions("post-bv-abstraction", d_assertionsToPreprocess);
+ dumpAssertions("post-bv-abstraction", d_assertions);
}
- dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
+ dumpAssertions("pre-boolean-terms", d_assertions);
{
Chat() << "rewriting Boolean terms..." << endl;
- for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
- d_assertionsToPreprocess[i] = rewriteBooleanTerms(d_assertionsToPreprocess[i]);
+ for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
+ d_assertions.replace(i, rewriteBooleanTerms(d_assertions[i]));
}
}
- dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
+ dumpAssertions("post-boolean-terms", d_assertions);
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess);
+ dumpAssertions("pre-constrain-subtypes", d_assertions);
{
// Any variables of subtype types need to be constrained properly.
// Careful, here: constrainSubtypes() adds to the back of
- // d_assertionsToPreprocess, but we don't need to reprocess those.
+ // d_assertions, but we don't need to reprocess those.
// We also can't use an iterator, because the vector may be moved in
// memory during this loop.
Chat() << "constraining subtypes..." << endl;
- for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
- constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess);
+ for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
+ constrainSubtypes(d_assertions[i], d_assertions);
}
}
- dumpAssertions("post-constrain-subtypes", d_assertionsToPreprocess);
+ dumpAssertions("post-constrain-subtypes", d_assertions);
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
+ bool noConflict = true;
// Unconstrained simplification
if(options::unconstrainedSimp()) {
- dumpAssertions("pre-unconstrained-simp", d_assertionsToPreprocess);
+ dumpAssertions("pre-unconstrained-simp", d_assertions);
Chat() << "...doing unconstrained simplification..." << endl;
- unconstrainedSimp(d_assertionsToPreprocess);
- dumpAssertions("post-unconstrained-simp", d_assertionsToPreprocess);
+ unconstrainedSimp();
+ dumpAssertions("post-unconstrained-simp", d_assertions);
}
if(options::bvIntroducePow2()){
- theory::bv::BVIntroducePow2::pow2Rewrite(d_assertionsToPreprocess);
+ theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
}
- dumpAssertions("pre-substitution", d_assertionsToPreprocess);
+ dumpAssertions("pre-substitution", d_assertions);
- // Apply the substitutions we already have, and normalize
- Chat() << "applying substitutions..." << endl;
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "applying substitutions" << endl;
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl;
- d_assertionsToPreprocess[i] =
- Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
- Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl;
+ if(options::unsatCores()) {
+ // special rewriting pass for unsat cores, since many of the passes below are skipped
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
+ }
+ } else {
+ // Apply the substitutions we already have, and normalize
+ if(!options::unsatCores()) {
+ Chat() << "applying substitutions..." << endl;
+ Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+ << "applying substitutions" << endl;
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Trace("simplify") << "applying to " << d_assertions[i] << endl;
+ d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
+ Trace("simplify") << " got " << d_assertions[i] << endl;
+ }
+ }
}
- dumpAssertions("post-substitution", d_assertionsToPreprocess);
- // Assertions ARE guaranteed to be rewritten by this point
+ dumpAssertions("post-substitution", d_assertions);
+ // Assertions ARE guaranteed to be rewritten by this point
// Lift bit-vectors of size 1 to bool
if(options::bitvectorToBool()) {
- dumpAssertions("pre-bv-to-bool", d_assertionsToPreprocess);
+ dumpAssertions("pre-bv-to-bool", d_assertions);
Chat() << "...doing bvToBool..." << endl;
bvToBool();
- dumpAssertions("post-bv-to-bool", d_assertionsToPreprocess);
+ dumpAssertions("post-bv-to-bool", d_assertions);
}
if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
- dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
+ dumpAssertions("pre-strings-pp", d_assertions);
CVC4::theory::strings::StringsPreprocess sp;
std::vector<Node> newNodes;
- newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]);
- sp.simplify( d_assertionsToPreprocess, newNodes );
+ newNodes.push_back(d_assertions[d_realAssertionsEnd - 1]);
+ sp.simplify( d_assertions.ref(), newNodes );
if(newNodes.size() > 1) {
- d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
+ d_assertions[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
}
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions[i] = Rewriter::rewrite( d_assertions[i] );
}
- dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
+ dumpAssertions("post-strings-pp", d_assertions);
}
if( d_smt.d_logic.isQuantified() ){
//remove rewrite rules
- for( unsigned i=0; i < d_assertionsToPreprocess.size(); i++ ) {
- if( d_assertionsToPreprocess[i].getKind() == kind::REWRITE_RULE ){
- Node prev = d_assertionsToPreprocess[i];
+ for( unsigned i=0; i < d_assertions.size(); i++ ) {
+ if( d_assertions[i].getKind() == kind::REWRITE_RULE ){
+ Node prev = d_assertions[i];
Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl;
- d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertionsToPreprocess[i] ) );
+ d_assertions[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) );
Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl;
- Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl;
+ Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl;
}
}
- dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
+ dumpAssertions("pre-skolem-quant", d_assertions);
if( options::preSkolemQuant() ){
//apply pre-skolemization to existential quantifiers
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
- Node prev = d_assertionsToPreprocess[i];
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Node prev = d_assertions[i];
Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
vector< TypeNode > fvTypes;
vector< TNode > fvs;
- d_assertionsToPreprocess[i] = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
- if( prev!=d_assertionsToPreprocess[i] ){
- d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+ d_assertions.replace(i, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ));
+ if( prev!=d_assertions[i] ){
+ d_assertions.replace(i, Rewriter::rewrite( d_assertions[i] ));
Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
- Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl;
+ Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl;
}
}
}
- dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
+ dumpAssertions("post-skolem-quant", d_assertions);
if( options::macrosQuant() ){
//quantifiers macro expansion
bool success;
do{
quantifiers::QuantifierMacros qm;
- success = qm.simplify( d_assertionsToPreprocess, true );
+ success = qm.simplify( d_assertions.ref(), true );
}while( success );
}
+ if( options::fmfFunWellDefined() ){
+ quantifiers::FunDefFmf fdf;
+ fdf.simplify( d_assertions.ref() );
+ }
Trace("fo-rsn-enable") << std::endl;
if( options::foPropQuant() ){
quantifiers::FirstOrderPropagation fop;
- fop.simplify( d_assertionsToPreprocess );
+ fop.simplify( d_assertions.ref() );
}
}
if( options::sortInference() ){
//sort inference technique
SortInference * si = d_smt.d_theoryEngine->getSortInference();
- si->simplify( d_assertionsToPreprocess );
+ si->simplify( d_assertions.ref() );
for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
d_smt.setPrintFuncInModel( it->first.toExpr(), false );
d_smt.setPrintFuncInModel( it->second.toExpr(), true );
@@ -3009,25 +3165,25 @@ void SmtEnginePrivate::processAssertions() {
}
//if( options::quantConflictFind() ){
- // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertionsToPreprocess );
+ // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertions );
//}
if( options::pbRewrites() ){
- d_pbsProcessor.learn(d_assertionsToPreprocess);
+ d_pbsProcessor.learn(d_assertions.ref());
if(d_pbsProcessor.likelyToHelp()){
- d_pbsProcessor.applyReplacements(d_assertionsToPreprocess);
+ d_pbsProcessor.applyReplacements(d_assertions.ref());
}
}
- dumpAssertions("pre-simplify", d_assertionsToPreprocess);
+ dumpAssertions("pre-simplify", d_assertions);
Chat() << "simplifying assertions..." << endl;
- bool noConflict = simplifyAssertions();
+ noConflict = simplifyAssertions();
if(!noConflict){
++(d_smt.d_stats->d_simplifiedToFalse);
}
- dumpAssertions("post-simplify", d_assertionsToCheck);
+ dumpAssertions("post-simplify", d_assertions);
- dumpAssertions("pre-static-learning", d_assertionsToCheck);
+ dumpAssertions("pre-static-learning", d_assertions);
if(options::doStaticLearning()) {
// Perform static learning
Chat() << "doing static learning..." << endl;
@@ -3035,27 +3191,25 @@ void SmtEnginePrivate::processAssertions() {
<< "performing static learning" << endl;
staticLearning();
}
- dumpAssertions("post-static-learning", d_assertionsToCheck);
+ dumpAssertions("post-static-learning", d_assertions);
Trace("smt") << "POST bvToBool" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- dumpAssertions("pre-ite-removal", d_assertionsToCheck);
+ dumpAssertions("pre-ite-removal", d_assertions);
{
Chat() << "removing term ITEs..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime);
// Remove ITEs, updating d_iteSkolemMap
- d_smt.d_stats->d_numAssertionsPre += d_assertionsToCheck.size();
+ d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
removeITEs();
- d_smt.d_stats->d_numAssertionsPost += d_assertionsToCheck.size();
+ d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
}
- dumpAssertions("post-ite-removal", d_assertionsToCheck);
+ dumpAssertions("post-ite-removal", d_assertions);
- dumpAssertions("pre-repeat-simplify", d_assertionsToCheck);
+ dumpAssertions("pre-repeat-simplify", d_assertions);
if(options::repeatSimp()) {
- d_assertionsToCheck.swap(d_assertionsToPreprocess);
Chat() << "re-simplifying assertions..." << endl;
ScopeCounter depth(d_simplifyAssertionsDepth);
noConflict &= simplifyAssertions();
@@ -3084,11 +3238,11 @@ void SmtEnginePrivate::processAssertions() {
IteSkolemMap::iterator it = d_iteSkolemMap.begin();
IteSkolemMap::iterator iend = d_iteSkolemMap.end();
NodeBuilder<> builder(kind::AND);
- builder << d_assertionsToCheck[d_realAssertionsEnd - 1];
+ builder << d_assertions[d_realAssertionsEnd - 1];
vector<TNode> toErase;
for (; it != iend; ++it) {
if (skolemSet.find((*it).first) == skolemSet.end()) {
- TNode iteExpr = d_assertionsToCheck[(*it).second];
+ TNode iteExpr = d_assertions[(*it).second];
if (iteExpr.getKind() == kind::ITE &&
iteExpr[1].getKind() == kind::EQUAL &&
iteExpr[1][0] == (*it).first &&
@@ -3104,8 +3258,8 @@ void SmtEnginePrivate::processAssertions() {
}
}
// Move this iteExpr into the main assertions
- builder << d_assertionsToCheck[(*it).second];
- d_assertionsToCheck[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
+ builder << d_assertions[(*it).second];
+ d_assertions[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
toErase.push_back((*it).first);
}
if(builder.getNumChildren() > 1) {
@@ -3113,60 +3267,58 @@ void SmtEnginePrivate::processAssertions() {
d_iteSkolemMap.erase(toErase.back());
toErase.pop_back();
}
- d_assertionsToCheck[d_realAssertionsEnd - 1] =
+ d_assertions[d_realAssertionsEnd - 1] =
Rewriter::rewrite(Node(builder));
}
// For some reason this is needed for some benchmarks, such as
// http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
// Figure it out later
removeITEs();
- // Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
+ // Assert(iteRewriteAssertionsEnd == d_assertions.size());
}
}
- dumpAssertions("post-repeat-simplify", d_assertionsToCheck);
+ dumpAssertions("post-repeat-simplify", d_assertions);
- dumpAssertions("pre-rewrite-apply-to-const", d_assertionsToCheck);
+ dumpAssertions("pre-rewrite-apply-to-const", d_assertions);
if(options::rewriteApplyToConst()) {
Chat() << "Rewriting applies to constants..." << endl;
- TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_assertionsToCheck[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertionsToCheck[i]));
+ TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteApplyToConstTime);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertions[i]));
}
}
- dumpAssertions("post-rewrite-apply-to-const", d_assertionsToCheck);
+ dumpAssertions("post-rewrite-apply-to-const", d_assertions);
// begin: INVARIANT to maintain: no reordering of assertions or
// introducing new ones
#ifdef CVC4_ASSERTIONS
- unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size();
+ unsigned iteRewriteAssertionsEnd = d_assertions.size();
#endif
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
- Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
- Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- dumpAssertions("pre-theory-preprocessing", d_assertionsToCheck);
+ dumpAssertions("pre-theory-preprocessing", d_assertions);
{
Chat() << "theory preprocessing..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
// Call the theory preprocessors
d_smt.d_theoryEngine->preprocessStart();
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
}
}
- dumpAssertions("post-theory-preprocessing", d_assertionsToCheck);
+ dumpAssertions("post-theory-preprocessing", d_assertions);
// If we are using eager bit-blasting wrap assertions in fake atom so that
// everything gets bit-blasted to internal SAT solver
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
- TNode atom = d_assertionsToCheck[i];
+ for (unsigned i = 0; i < d_assertions.size(); ++i) {
+ TNode atom = d_assertions[i];
Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
- d_assertionsToCheck[i] = eager_atom;
+ d_assertions.replace(i, eager_atom);
TheoryModel* m = d_smt.d_theoryEngine->getModel();
m->addSubstitution(eager_atom, atom);
}
@@ -3175,28 +3327,36 @@ void SmtEnginePrivate::processAssertions() {
// Push the formula to decision engine
if(noConflict) {
Chat() << "pushing to decision engine..." << endl;
- Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
+ Assert(iteRewriteAssertionsEnd == d_assertions.size());
d_smt.d_decisionEngine->addAssertions
- (d_assertionsToCheck, d_realAssertionsEnd, d_iteSkolemMap);
+ (d_assertions.ref(), d_realAssertionsEnd, d_iteSkolemMap);
}
// end: INVARIANT to maintain: no reordering of assertions or
// introducing new ones
- dumpAssertions("post-everything", d_assertionsToCheck);
-
+ dumpAssertions("post-everything", d_assertions);
+
+ //set instantiation level of everything to zero
+ if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
+ for( unsigned i=0; i < d_assertions.size(); i++ ) {
+ theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions[i], 0 );
+ }
+ }
+
// Push the formula to SAT
{
Chat() << "converting to CNF..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
- for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
- d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Chat() << "+ " << d_assertions[i] << std::endl;
+ d_smt.d_propEngine->assertFormula(d_assertions[i]);
}
}
d_assertionsProcessed = true;
- d_assertionsToCheck.clear();
+ d_assertions.clear();
d_iteSkolemMap.clear();
}
@@ -3211,13 +3371,8 @@ void SmtEnginePrivate::addFormula(TNode n)
Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
// Add the normalized formula to the queue
- d_assertionsToPreprocess.push_back(n);
- //d_assertionsToPreprocess.push_back(Rewriter::rewrite(n));
-
- // If the mode of processing is incremental prepreocess and assert immediately
- if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL) {
- processAssertions();
- }
+ d_assertions.push_back(n);
+ //d_assertions.push_back(Rewriter::rewrite(n));
}
void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
@@ -3232,7 +3387,7 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
}
}
-Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
+Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
@@ -3253,7 +3408,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
// Ensure expr is type-checked at this point.
ensureBoolean(e);
// Give it to proof manager
- PROOF( ProofManager::currentPM()->addAssertion(e); );
+ PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); );
}
// check to see if a postsolve() is pending
@@ -3315,7 +3470,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
return r;
}/* SmtEngine::checkSat() */
-Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
+Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
Assert(!ex.isNull());
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
@@ -3334,7 +3489,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
// Ensure that the expression is type-checked at this point, and Boolean
ensureBoolean(e);
// Give it to proof manager
- PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); );
+ PROOF( ProofManager::currentPM()->addAssertion(e.notExpr(), inUnsatCore); );
// check to see if a postsolve() is pending
if(d_needPostsolve) {
@@ -3393,13 +3548,13 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
return r;
}/* SmtEngine::query() */
-Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) {
+Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException) {
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
- PROOF( ProofManager::currentPM()->addAssertion(ex); );
+ PROOF( ProofManager::currentPM()->addAssertion(ex, inUnsatCore); );
Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
@@ -3412,12 +3567,11 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
}
d_private->addFormula(e.getNode());
return quickCheck().asValidityResult();
-}
+}/* SmtEngine::assertFormula() */
Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
ModelPostprocessor mpost;
NodeVisitor<ModelPostprocessor> visitor;
- Debug("boolean-terms") << "postproc: visit " << node << endl;
Node value = visitor.run(mpost, node);
Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
Node realValue = mpost.rewriteAs(value, expectedType);
@@ -3540,6 +3694,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
if(options::abstractValues() && resultNode.getType().isArray()) {
resultNode = d_private->mkAbstractValue(resultNode);
+ Trace("smt") << "--- abstract value >> " << resultNode << endl;
}
return resultNode.toExpr();
@@ -3704,8 +3859,8 @@ Model* SmtEngine::getModel() throw(ModalException) {
}
void SmtEngine::checkModel(bool hardFailure) {
- // --check-model implies --interactive, which enables the assertion list,
- // so we should be ok.
+ // --check-model implies --produce-assertions, 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_stats->d_checkModelTime);
@@ -3883,6 +4038,30 @@ void SmtEngine::checkModel(bool hardFailure) {
Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
}
+UnsatCore SmtEngine::getUnsatCore() throw(ModalException) {
+ Trace("smt") << "SMT getUnsatCore()" << endl;
+ SmtScope smts(this);
+ finalOptionsAreSet();
+ if(Dump.isOn("benchmark")) {
+ Dump("benchmark") << GetUnsatCoreCommand();
+ }
+#ifdef CVC4_PROOF
+ if(!options::unsatCores()) {
+ throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off.");
+ }
+ if(d_status.isNull() ||
+ d_status.asSatisfiabilityResult() != Result::UNSAT ||
+ d_problemExtended) {
+ throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.");
+ }
+
+ d_proofManager->getProof(this);// just to trigger core creation
+ return UnsatCore(this, d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core());
+#else /* CVC4_PROOF */
+ throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
+#endif /* CVC4_PROOF */
+}
+
Proof* SmtEngine::getProof() throw(ModalException) {
Trace("smt") << "SMT getProof()" << endl;
SmtScope smts(this);
@@ -3892,16 +4071,12 @@ Proof* SmtEngine::getProof() throw(ModalException) {
}
#ifdef CVC4_PROOF
if(!options::proof()) {
- const char* msg =
- "Cannot get a proof when produce-proofs option is off.";
- throw ModalException(msg);
+ throw ModalException("Cannot get a proof when produce-proofs option is off.");
}
if(d_status.isNull() ||
d_status.asSatisfiabilityResult() != Result::UNSAT ||
d_problemExtended) {
- const char* msg =
- "Cannot get a proof unless immediately preceded by UNSAT/VALID response.";
- throw ModalException(msg);
+ throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response.");
}
return ProofManager::getProof(this);
@@ -3930,9 +4105,9 @@ vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
Dump("benchmark") << GetAssertionsCommand();
}
Trace("smt") << "SMT getAssertions()" << endl;
- if(!options::interactive()) {
+ if(!options::produceAssertions()) {
const char* msg =
- "Cannot query the current assertion list when not in interactive mode.";
+ "Cannot query the current assertion list when not in produce-assertions mode.";
throw ModalException(msg);
}
Assert(d_assertionList != NULL);
@@ -4049,6 +4224,40 @@ void SmtEngine::doPendingPops() {
}
}
+void SmtEngine::reset() throw() {
+ SmtScope smts(this);
+ ExprManager *em = d_exprManager;
+ Trace("smt") << "SMT reset()" << endl;
+ if(Dump.isOn("benchmark")) {
+ Dump("benchmark") << ResetCommand();
+ }
+ Options opts = d_originalOptions;
+ this->~SmtEngine();
+ NodeManager::fromExprManager(em)->getOptions() = opts;
+ new(this) SmtEngine(em);
+}
+
+void SmtEngine::resetAssertions() throw() {
+ SmtScope smts(this);
+
+ Trace("smt") << "SMT resetAssertions()" << endl;
+ if(Dump.isOn("benchmark")) {
+ Dump("benchmark") << ResetAssertionsCommand();
+ }
+
+ while(!d_userLevels.empty()) {
+ pop();
+ }
+
+ // Also remember the global push/pop around everything.
+ Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
+ d_context->popto(0);
+ d_userContext->popto(0);
+ d_modelGlobalCommands.clear();
+ d_userContext->push();
+ d_context->push();
+}
+
void SmtEngine::interrupt() throw(ModalException) {
if(!d_fullyInited) {
return;
@@ -4111,9 +4320,13 @@ SExpr SmtEngine::getStatistic(std::string name) const throw() {
return d_statisticsRegistry->getStatistic(name);
}
-void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) {
+void SmtEngine::setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value) {
SmtScope smts(this);
- d_theoryEngine->setUserAttribute(attr, expr.getNode());
+ std::vector<Node> node_values;
+ for( unsigned i=0; i<expr_values.size(); i++ ){
+ node_values.push_back( expr_values[i].getNode() );
+ }
+ d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
}
void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 71b42534a..489d34d79 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,6 +28,7 @@
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/proof.h"
+#include "util/unsat_core.h"
#include "smt/modal_exception.h"
#include "smt/logic_exception.h"
#include "options/options.h"
@@ -70,6 +71,13 @@ namespace prop {
class PropEngine;
}/* CVC4::prop namespace */
+namespace expr {
+ namespace attr {
+ class AttributeManager;
+ struct SmtAttributes;
+ }/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
namespace smt {
/**
* Representation of a defined function. We keep these around in
@@ -182,6 +190,11 @@ class CVC4_PUBLIC SmtEngine {
LogicInfo d_logic;
/**
+ * Keep a copy of the original option settings (for reset()).
+ */
+ Options d_originalOptions;
+
+ /**
* Number of internal pops that have been deferred.
*/
unsigned d_pendingPops;
@@ -255,7 +268,7 @@ class CVC4_PUBLIC SmtEngine {
smt::SmtEnginePrivate* d_private;
/**
- * Check that a generated Proof (via getProof()) checks.
+ * Check that a generated proof (via getProof()) checks.
*/
void checkProof();
@@ -341,9 +354,20 @@ class CVC4_PUBLIC SmtEngine {
// to access d_modelCommands
friend class ::CVC4::Model;
friend class ::CVC4::theory::TheoryModel;
+ // to access SmtAttributes
+ friend class expr::attr::AttributeManager;
// to access getModel(), which is private (for now)
friend class GetModelCommand;
+ /**
+ * There's something of a handshake between the expr package's
+ * AttributeManager and the SmtEngine because the expr package
+ * doesn't have a Context on its own (that's owned by the
+ * SmtEngine). Thus all context-dependent attributes are stored
+ * here.
+ */
+ expr::attr::SmtAttributes* d_smtAttributes;
+
StatisticsRegistry* d_statisticsRegistry;
smt::SmtEngineStatistics* d_stats;
@@ -424,8 +448,8 @@ public:
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
- * literals and conjunction of literals. Returns false iff
- * inconsistent.
+ * literals and conjunction of literals. Returns false if
+ * immediately determined to be inconsistent.
*/
void defineFunction(Expr func,
const std::vector<Expr>& formals,
@@ -434,23 +458,25 @@ public:
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
- * literals and conjunction of literals. Returns false iff
- * inconsistent.
+ * literals and conjunction of literals. Returns false if
+ * immediately determined to be inconsistent. This version
+ * takes a Boolean flag to determine whether to include this asserted
+ * formula in an unsat core (if one is later requested).
*/
- Result assertFormula(const Expr& e) throw(TypeCheckingException, LogicException);
+ Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException);
/**
* Check validity of an expression with respect to the current set
* of assertions by asserting the query expression's negation and
* calling check(). Returns valid, invalid, or unknown result.
*/
- Result query(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
+ Result query(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
/**
* Assert a formula (if provided) to the current context and call
* check(). Returns sat, unsat, or unknown result.
*/
- Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException, LogicException);
+ Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
/**
* Simplify a formula without doing "much" work. Does not involve
@@ -507,6 +533,13 @@ public:
void printInstantiations( std::ostream& out );
/**
+ * Get an unsatisfiable core (only if immediately preceded by an
+ * UNSAT or VALID query). Only permitted if CVC4 was built with
+ * unsat-core support and produce-unsat-cores is on.
+ */
+ UnsatCore getUnsatCore() throw(ModalException);
+
+ /**
* Get the current set of assertions. Only permitted if the
* SmtEngine is set to operate interactively.
*/
@@ -523,6 +556,18 @@ public:
void pop() throw(ModalException);
/**
+ * Completely reset the state of the solver, as though destroyed and
+ * recreated. The result is as if newly constructed (so it still
+ * retains the same options structure and ExprManager).
+ */
+ void reset() throw();
+
+ /**
+ * Reset all assertions, global declarations, etc.
+ */
+ void resetAssertions() throw();
+
+ /**
* Interrupt a running query. This can be called from another thread
* or from a signal handler. Throws a ModalException if the SmtEngine
* isn't currently in a query.
@@ -651,7 +696,7 @@ public:
* This function is called when an attribute is set by a user.
* In SMT-LIBv2 this is done via the syntax (! expr :attr)
*/
- void setUserAttribute(const std::string& attr, Expr expr);
+ void setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value);
/**
* Set print function in model
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 54b9fa1d0..fb5810fd5 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -40,9 +40,14 @@ inline SmtEngine* currentSmtEngine() {
}
inline ProofManager* currentProofManager() {
- Assert(PROOF_ON());
+#ifdef CVC4_PROOF
+ Assert(options::proof() || options::unsatCores());
Assert(s_smtEngine_current != NULL);
return s_smtEngine_current->d_proofManager;
+#else /* CVC4_PROOF */
+ InternalError("proofs/unsat cores are not on, but ProofManager requested");
+ return NULL;
+#endif /* CVC4_PROOF */
}
class SmtScope : public NodeManagerScope {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback