diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 5 | ||||
-rw-r--r-- | src/main/options_handlers.h | 3 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 33 | ||||
-rw-r--r-- | src/util/configuration.cpp | 6 | ||||
-rw-r--r-- | src/util/configuration.h | 4 | ||||
-rw-r--r-- | src/util/configuration_private.h | 8 |
7 files changed, 38 insertions, 23 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 34fa20c1d..9531db0ce 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -433,6 +433,11 @@ if CVC4_USE_GLPK libcvc4_la_LIBADD += $(GLPK_LIBS) endif +if CVC4_USE_ABC +libcvc4_la_LIBADD += $(ABC_LIBS) +libcvc4_la_LDFLAGS += $(ABC_LDFLAGS) +endif + BUILT_SOURCES = \ theory/rewriter_tables.h \ theory/theory_traits.h \ diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h index 7723dcb33..ee16af2f2 100644 --- a/src/main/options_handlers.h +++ b/src/main/options_handlers.h @@ -65,8 +65,9 @@ inline void showConfiguration(std::string option, SmtEngine* smt) { printf("\n"); printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); - printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); + printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); + printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); } diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index a5fe46d27..ebf36b0cd 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -95,7 +95,7 @@ std::pair<int, S> runPortfolio(int numThreads, for(int t = 0; t < numThreads; ++t) { if(optionWaitToJoin) { threads[t].join(); - } + } } std::pair<int, S> retval(global_winner, threads_returnValue[global_winner]); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b71969d15..6ab25ee57 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -367,9 +367,9 @@ private: void bvToBool(); // Abstract common structure over small domains to UF - // return true if changes were made. - void bvAbstraction(); - + // return true if changes were made. + void bvAbstraction(); + // Simplify ITE structure bool simpITE(); @@ -1085,7 +1085,7 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl; setOption("incremental", SExpr("false")); } - + if (! options::bvEagerExplanations.wasSetByUser() && d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV)) { @@ -1093,8 +1093,6 @@ void SmtEngine::setDefaults() { options::bvEagerExplanations.set(true); } - - // Turn on arith rewrite equalities only for pure arithmetic if(! options::arithRewriteEq.wasSetByUser()) { bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified(); @@ -2006,11 +2004,11 @@ void SmtEnginePrivate::bvAbstraction() { d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]); } // if we are using the lazy solver and the abstraction - // applies, then UF symbols were introduced + // applies, then UF symbols were introduced if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && changed) { LogicRequest req(d_smt); - req.widenLogic(THEORY_UF); + req.widenLogic(THEORY_UF); } } @@ -2577,7 +2575,7 @@ bool SmtEnginePrivate::simplifyAssertions() // before ppRewrite check if only core theory for BV theory d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertionsToCheck); - + // Theory preprocessing if (d_smt.d_earlyTheoryPP) { Chat() << "...doing early theory preprocessing..." << endl; @@ -2870,18 +2868,17 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && !d_smt.d_logic.isPure(THEORY_BV)) { throw ModalException("Eager bit-blasting does not currently support theory combination. " "Note that in a QF_BV problem UF symbols can be introduced for division. " - "Try --bv-div-zero-const to interpret division by zero as a constant."); + "Try --bv-div-zero-const to interpret division by zero as a constant."); } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess); + d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess); } - if ( options::bvAbstraction() && !options::incrementalSolving()) { @@ -2889,7 +2886,7 @@ void SmtEnginePrivate::processAssertions() { bvAbstraction(); dumpAssertions("post-bv-abstraction", d_assertionsToPreprocess); } - + dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess); { Chat() << "rewriting Boolean terms..." << endl; @@ -2952,7 +2949,7 @@ void SmtEnginePrivate::processAssertions() { bvToBool(); dumpAssertions("post-bv-to-bool", d_assertionsToPreprocess); } - + if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { dumpAssertions("pre-strings-pp", d_assertionsToPreprocess); CVC4::theory::strings::StringsPreprocess sp; @@ -3174,10 +3171,10 @@ void SmtEnginePrivate::processAssertions() { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) { Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, d_assertionsToCheck[i]); - d_assertionsToCheck[i] = eager_atom; + d_assertionsToCheck[i] = eager_atom; } } - + // Push the formula to decision engine if(noConflict) { Chat() << "pushing to decision engine..." << endl; @@ -3191,6 +3188,7 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-everything", d_assertionsToCheck); + // Push the formula to SAT { Chat() << "converting to CNF..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime); @@ -3198,7 +3196,6 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); } } - d_assertionsProcessed = true; diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 0d22325e7..05f5c7678 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Liana Hadarean, Tim King, ACSYS, Christopher L. Conway, Dejan Jovanovic, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -125,6 +125,10 @@ bool Configuration::isBuiltWithGlpk() { return IS_GLPK_BUILD; } +bool Configuration::isBuiltWithAbc() { + return IS_ABC_BUILD; +} + bool Configuration::isBuiltWithCudd() { return false; } diff --git a/src/util/configuration.h b/src/util/configuration.h index 696b67715..c6562b3e6 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): ACSYS, Liana Hadarean, Tim King, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -91,6 +91,8 @@ public: static bool isBuiltWithGlpk(); + static bool isBuiltWithAbc(); + static bool isBuiltWithReadline(); static bool isBuiltWithCudd(); diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 07ab4b17e..631a323d3 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -5,7 +5,7 @@ ** Major contributors: ACSYS, Morgan Deters ** Minor contributors (to current version): Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -107,6 +107,12 @@ namespace CVC4 { # define IS_GLPK_BUILD false #endif /* CVC4_USE_GLPK */ +#if CVC4_USE_ABC +# define IS_ABC_BUILD true +#else /* CVC4_USE_ABC */ +# define IS_ABC_BUILD false +#endif /* CVC4_USE_ABC */ + #ifdef HAVE_LIBREADLINE # define IS_READLINE_BUILD true #else /* HAVE_LIBREADLINE */ |