summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp218
1 files changed, 43 insertions, 175 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0d93c16bc..951b49603 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -79,8 +79,11 @@
#include "preprocessing/passes/bv_intro_pow2.h"
#include "preprocessing/passes/bv_to_bool.h"
#include "preprocessing/passes/extended_rewriter_pass.h"
+#include "preprocessing/passes/global_negate.h"
#include "preprocessing/passes/int_to_bv.h"
#include "preprocessing/passes/ite_removal.h"
+#include "preprocessing/passes/ite_simp.h"
+#include "preprocessing/passes/nl_ext_purify.h"
#include "preprocessing/passes/pseudo_boolean_processor.h"
#include "preprocessing/passes/quantifiers_preprocess.h"
#include "preprocessing/passes/real_to_int.h"
@@ -116,7 +119,6 @@
#include "theory/bv/theory_bv_rewriter.h"
#include "theory/logic_info.h"
#include "theory/quantifiers/fun_def_process.h"
-#include "theory/quantifiers/global_negate.h"
#include "theory/quantifiers/macros.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/single_inv_partition.h"
@@ -202,8 +204,6 @@ struct SmtEngineStatistics {
IntStat d_numMiplibAssertionsRemoved;
/** number of constant propagations found during nonclausal simp */
IntStat d_numConstantProps;
- /** time spent in simplifying ITEs */
- TimerStat d_simpITETime;
/** time spent in theory preprocessing */
TimerStat d_theoryPreprocessTime;
/** time spent converting to CNF */
@@ -236,7 +236,6 @@ struct SmtEngineStatistics {
d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
- d_simpITETime("smt::SmtEngine::simpITETime"),
d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
@@ -255,7 +254,6 @@ struct SmtEngineStatistics {
smtStatisticsRegistry()->registerStat(&d_miplibPassTime);
smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
smtStatisticsRegistry()->registerStat(&d_numConstantProps);
- smtStatisticsRegistry()->registerStat(&d_simpITETime);
smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime);
smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
@@ -276,7 +274,6 @@ struct SmtEngineStatistics {
smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime);
smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
- smtStatisticsRegistry()->unregisterStat(&d_simpITETime);
smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime);
smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
@@ -567,14 +564,6 @@ class SmtEnginePrivate : public NodeManagerListener {
bool nonClausalSimplify();
/**
- * Performs static learning on the assertions.
- */
- void staticLearning();
-
- Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq);
- Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false);
-
- /**
* Helper function to fix up assertion list to restore invariants needed after
* ite removal.
*/
@@ -586,15 +575,6 @@ class SmtEnginePrivate : public NodeManagerListener {
*/
bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
- // Simplify ITE structure
- bool simpITE();
-
- /**
- * Ensures the assertions asserted after before now effectively come before
- * d_realAssertionsEnd.
- */
- void compressBeforeRealAssertions(size_t before);
-
/**
* Trace nodes back to their assertions using CircuitPropagator's
* BackEdgesMap.
@@ -740,10 +720,14 @@ class SmtEnginePrivate : public NodeManagerListener {
}
}
- void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override
+ void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts,
+ uint32_t flags) override
{
- DatatypeDeclarationCommand c(dtts);
- d_smt.addToModelCommandAndDump(c);
+ if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
+ {
+ DatatypeDeclarationCommand c(dtts);
+ d_smt.addToModelCommandAndDump(c);
+ }
}
void nmNotifyNewVar(TNode n, uint32_t flags) override
@@ -792,7 +776,7 @@ class SmtEnginePrivate : public NodeManagerListener {
/** Process a user push.
*/
void notifyPush() {
-
+
}
/**
@@ -874,13 +858,13 @@ class SmtEnginePrivate : public NodeManagerListener {
std::ostream* getReplayLog() const {
return d_managedReplayLog.getReplayLog();
}
-
+
//------------------------------- expression names
// implements setExpressionName, as described in smt_engine.h
void setExpressionName(Expr e, std::string name) {
d_exprNames[Node::fromExpr(e)] = name;
}
-
+
// implements getExpressionName, as described in smt_engine.h
bool getExpressionName(Expr e, std::string& name) const {
context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e);
@@ -1192,6 +1176,8 @@ void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
LogicInfo SmtEngine::getLogicInfo() const {
return d_logic;
}
+void SmtEngine::setFilename(std::string filename) { d_filename = filename; }
+std::string SmtEngine::getFilename() const { return d_filename; }
void SmtEngine::setLogicInternal()
{
Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already"
@@ -2026,7 +2012,6 @@ void SmtEngine::setDefaults() {
}
if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
{
- options::cbqiAll.set( false );
if( !options::quantConflictFind.wasSetByUser() ){
options::quantConflictFind.set( false );
}
@@ -2301,15 +2286,14 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
}
// Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
- if (key == "source"
- || key == "category"
- || key == "difficulty"
- || key == "notes"
- || key == "license")
+ if (key == "source" || key == "category" || key == "difficulty"
+ || key == "notes" || key == "name" || key == "license")
{
// ignore these
return;
- } else if(key == "name") {
+ }
+ else if (key == "filename")
+ {
d_filename = value.getValue();
return;
}
@@ -2653,8 +2637,14 @@ void SmtEnginePrivate::finishInit()
new BVToBool(d_preprocessingPassContext.get()));
std::unique_ptr<ExtRewPre> extRewPre(
new ExtRewPre(d_preprocessingPassContext.get()));
+ std::unique_ptr<GlobalNegate> globalNegate(
+ new GlobalNegate(d_preprocessingPassContext.get()));
std::unique_ptr<IntToBV> intToBV(
new IntToBV(d_preprocessingPassContext.get()));
+ std::unique_ptr<ITESimp> iteSimp(
+ new ITESimp(d_preprocessingPassContext.get()));
+ std::unique_ptr<NlExtPurify> nlExtPurify(
+ new NlExtPurify(d_preprocessingPassContext.get()));
std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
new QuantifiersPreprocess(d_preprocessingPassContext.get()));
std::unique_ptr<PseudoBooleanProcessor> pbProc(
@@ -2696,7 +2686,12 @@ void SmtEnginePrivate::finishInit()
std::move(bvIntroPow2));
d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool));
d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre));
+ d_preprocessingPassRegistry.registerPass("global-negate",
+ std::move(globalNegate));
d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
+ d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp));
+ d_preprocessingPassRegistry.registerPass("nl-ext-purify",
+ std::move(nlExtPurify));
d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
std::move(quantifiersPreprocess));
d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
@@ -2709,7 +2704,7 @@ void SmtEnginePrivate::finishInit()
std::move(sepSkolemEmp));
d_preprocessingPassRegistry.registerPass("sort-inference",
std::move(sortInfer));
- d_preprocessingPassRegistry.registerPass("static-learning",
+ d_preprocessingPassRegistry.registerPass("static-learning",
std::move(staticLearning));
d_preprocessingPassRegistry.registerPass("sygus-infer",
std::move(sygusInfer));
@@ -2902,68 +2897,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
return result.top();
}
-typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-
-Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector< Node >& var_eq, bool beneathMult) {
- if( beneathMult ){
- NodeMap::iterator find = bcache.find(n);
- if (find != bcache.end()) {
- return (*find).second;
- }
- }else{
- NodeMap::iterator find = cache.find(n);
- if (find != cache.end()) {
- return (*find).second;
- }
- }
- Node ret = n;
- if( n.getNumChildren()>0 ){
- if (beneathMult
- && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
- {
- // don't do it if it rewrites to a constant
- Node nr = Rewriter::rewrite(n);
- if (nr.isConst())
- {
- // return the rewritten constant
- ret = nr;
- }
- else
- {
- // new variable
- ret = NodeManager::currentNM()->mkSkolem(
- "__purifyNl_var",
- n.getType(),
- "Variable introduced in purifyNl pass");
- Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
- var_eq.push_back(np.eqNode(ret));
- Trace("nl-ext-purify")
- << "Purify : " << ret << " -> " << np << std::endl;
- }
- }
- else
- {
- bool beneathMultNew = beneathMult || n.getKind()==kind::MULT;
- bool childChanged = false;
- std::vector< Node > children;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nc = purifyNlTerms( n[i], cache, bcache, var_eq, beneathMultNew );
- childChanged = childChanged || nc!=n[i];
- children.push_back( nc );
- }
- if( childChanged ){
- ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
- }
- if( beneathMult ){
- bcache[n] = ret;
- }else{
- cache[n] = ret;
- }
- return ret;
-}
-
// do dumping (before/after any preprocessing pass)
static void dumpAssertions(const char* key,
const AssertionPipeline& assertionList) {
@@ -3314,60 +3247,6 @@ bool SmtEnginePrivate::nonClausalSimplify() {
return true;
}
-bool SmtEnginePrivate::simpITE() {
- TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
-
- spendResource(options::preprocessStep());
-
- Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
-
- unsigned numAssertionOnEntry = d_assertions.size();
- for (unsigned i = 0; i < d_assertions.size(); ++i) {
- spendResource(options::preprocessStep());
- 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_assertions.ref());
- if(numAssertionOnEntry < d_assertions.size()){
- compressBeforeRealAssertions(numAssertionOnEntry);
- }
- return result;
-}
-
-void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
- size_t curr = d_assertions.size();
- if (before >= curr || d_assertions.getRealAssertionsEnd() <= 0
- || d_assertions.getRealAssertionsEnd() >= curr)
- {
- return;
- }
-
- // assertions
- // original: [0 ... d_assertions.getRealAssertionsEnd())
- // can be modified
- // ites skolems [d_assertions.getRealAssertionsEnd(), before)
- // cannot be moved
- // added [before, curr)
- // can be modified
- Assert(0 < d_assertions.getRealAssertionsEnd());
- Assert(d_assertions.getRealAssertionsEnd() <= before);
- Assert(before < curr);
-
- std::vector<Node> intoConjunction;
- for(size_t i = before; i<curr; ++i){
- intoConjunction.push_back(d_assertions[i]);
- }
- d_assertions.resize(before);
- size_t lastBeforeItes = d_assertions.getRealAssertionsEnd() - 1;
- intoConjunction.push_back(d_assertions[lastBeforeItes]);
- Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
- d_assertions.replace(lastBeforeItes, newLast);
- Assert(d_assertions.size() == before);
-}
-
void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) {
const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) {
@@ -3832,11 +3711,14 @@ bool SmtEnginePrivate::simplifyAssertions()
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// ITE simplification
- if(options::doITESimp() &&
- (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) {
+ if (options::doITESimp()
+ && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
+ {
Chat() << "...doing ITE simplification..." << endl;
- bool noConflict = simpITE();
- if(!noConflict){
+ PreprocessingPassResult res =
+ d_preprocessingPassRegistry.getPass("ite-simp")->apply(&d_assertions);
+ if (res == PreprocessingPassResult::CONFLICT)
+ {
Chat() << "...ITE simplification found unsat..." << endl;
return false;
}
@@ -4071,26 +3953,12 @@ void SmtEnginePrivate::processAssertions() {
if (options::globalNegate())
{
// global negation of the formula
- quantifiers::GlobalNegate gn;
- gn.simplify(d_assertions.ref());
+ d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions);
d_smt.d_globalNegation = !d_smt.d_globalNegation;
}
if( options::nlExtPurify() ){
- unordered_map<Node, Node, NodeHashFunction> cache;
- unordered_map<Node, Node, NodeHashFunction> bcache;
- std::vector< Node > var_eq;
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- Node a = d_assertions[i];
- d_assertions.replace(i, purifyNlTerms(a, cache, bcache, var_eq));
- Trace("nl-ext-purify")
- << "Purify : " << a << " -> " << d_assertions[i] << std::endl;
- }
- if( !var_eq.empty() ){
- unsigned lastIndex = d_assertions.size()-1;
- var_eq.insert( var_eq.begin(), d_assertions[lastIndex] );
- d_assertions.replace(lastIndex, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) );
- }
+ d_preprocessingPassRegistry.getPass("nl-ext-purify")->apply(&d_assertions);
}
if( options::ceGuidedInst() ){
@@ -5564,7 +5432,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
Assert( inst_qs.size()<=1 );
Node ret_n;
if( inst_qs.size()==1 ){
- Node top_q = inst_qs[0];
+ Node top_q = inst_qs[0];
//Node top_q = Rewriter::rewrite( nn_e ).negate();
Assert( top_q.getKind()==kind::FORALL );
Trace("smt-qe") << "Get qe for " << top_q << std::endl;
@@ -5987,7 +5855,7 @@ void SmtEngine::setReplayStream(ExprStream* replayStream) {
AlwaysAssert(!d_fullyInited,
"Cannot set replay stream once fully initialized");
d_replayStream = replayStream;
-}
+}
bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
return d_private->getExpressionName(e, name);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback