diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-22 18:01:22 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-22 18:01:22 -0700 |
| commit | 474faec211db41b626ed29d8dde26ff861f40d87 (patch) | |
| tree | 3c5e68fb24113fca9e74c002614a388698d9a5f5 /src | |
| parent | 0bb3e14b46a4b2f5cacfadb313c947da73ba7df6 (diff) | |
| parent | 21ee0f18c288d430d08c133f601173be25411187 (diff) | |
Merge branch 'master' into rmTearDownIncrementalrmTearDownIncremental
Diffstat (limited to 'src')
110 files changed, 1908 insertions, 1600 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index bec3a8345..74db7c941 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -441,6 +441,7 @@ libcvc5_add_sources( theory/arith/nl/nonlinear_extension.h theory/arith/nl/poly_conversion.cpp theory/arith/nl/poly_conversion.h + theory/arith/nl/pow2_solver.cpp theory/arith/nl/pow2_solver.h theory/arith/nl/stats.cpp theory/arith/nl/stats.h @@ -595,6 +596,7 @@ libcvc5_add_sources( theory/bv/bv_subtheory_core.h theory/bv/bv_subtheory_inequality.cpp theory/bv/bv_subtheory_inequality.h + theory/bv/int_blaster.cpp theory/bv/int_blaster.h theory/bv/proof_checker.cpp theory/bv/proof_checker.h @@ -1184,9 +1186,9 @@ if(USE_ABC) target_link_libraries(cvc5 PRIVATE ${ABC_LIBRARIES}) target_include_directories(cvc5 PRIVATE ${ABC_INCLUDE_DIR}) endif() -if(USE_CADICAL) - target_link_libraries(cvc5 PRIVATE CaDiCaL) -endif() + +target_link_libraries(cvc5 PRIVATE CaDiCaL) + if(USE_CLN) target_link_libraries(cvc5 PRIVATE CLN) endif() @@ -1203,9 +1205,8 @@ endif() if(USE_POLY) target_link_libraries(cvc5 PRIVATE Polyxx) endif() -if(USE_SYMFPU) - target_link_libraries(cvc5 PRIVATE SymFPU) -endif() + +target_link_libraries(cvc5 PRIVATE SymFPU) # Note: When linked statically GMP needs to be linked after CLN since CLN # depends on GMP. diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 668fc9382..43bb3d2dc 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -55,6 +55,7 @@ #include "expr/sequence.h" #include "expr/type_node.h" #include "expr/uninterpreted_constant.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/option_exception.h" #include "options/options.h" @@ -5196,18 +5197,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const << " children (the one under construction has " << nchildren << ")"; } -/* Solver Configuration */ -/* -------------------------------------------------------------------------- */ - -bool Solver::supportsFloatingPoint() const -{ - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return Configuration::isBuiltWithSymFPU(); - //////// - CVC5_API_TRY_CATCH_END; -} - /* Sorts Handling */ /* -------------------------------------------------------------------------- */ @@ -5275,8 +5264,6 @@ Sort Solver::getRoundingModeSort(void) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return Sort(this, getNodeManager()->roundingModeType()); //////// @@ -5313,8 +5300,6 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0"; //////// all checks before this line @@ -5793,8 +5778,6 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), false)); @@ -5806,8 +5789,6 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), true)); @@ -5819,8 +5800,6 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeNaN(FloatingPointSize(exp, sig))); @@ -5832,8 +5811,6 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), false)); @@ -5845,8 +5822,6 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); @@ -5858,8 +5833,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::RoundingMode>(s_rmodes.at(rm)); //////// @@ -5913,8 +5886,6 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; CVC5_API_SOLVER_CHECK_TERM(val); CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; @@ -6452,7 +6423,7 @@ Result Solver::checkEntailed(const Term& term) const NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); @@ -6468,7 +6439,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); @@ -6497,7 +6468,7 @@ Result Solver::checkSat(void) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line @@ -6512,7 +6483,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); @@ -6528,7 +6499,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 - || d_smtEngine->getOptions().smt.incrementalSolving) + || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); @@ -6863,7 +6834,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) + CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions) @@ -7044,7 +7015,7 @@ void Solver::pop(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) + CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot pop when not solving incrementally (use --incremental)"; CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) << "Cannot pop beyond first pushed context"; @@ -7176,7 +7147,7 @@ void Solver::push(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) + CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot push when not solving incrementally (use --incremental)"; //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index a1421cf12..161522654 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2752,12 +2752,6 @@ class CVC5_EXPORT Solver Solver& operator=(const Solver&) = delete; /* .................................................................... */ - /* Solver Configuration */ - /* .................................................................... */ - - bool supportsFloatingPoint() const; - - /* .................................................................... */ /* Sorts Handling */ /* .................................................................... */ diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 2ec190360..2c5d2873e 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -412,6 +412,22 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ IAND, + /** + * Operator for raising 2 to a non-negative integer power + * + * Create with: + * - `Solver::mkOp(Kind kind) const` + * + + * Parameters: + * - 1: Op of kind IAND + * - 2: Integer term + * + * Create with: + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` + */ + POW2, #if 0 /* Synonym for MULT. */ NONLINEAR_MULT, diff --git a/src/api/java/cvc5/Grammar.java b/src/api/java/cvc5/Grammar.java new file mode 100644 index 000000000..f8c6b05c5 --- /dev/null +++ b/src/api/java/cvc5/Grammar.java @@ -0,0 +1,87 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +public class Grammar extends AbstractPointer { + // region construction and destruction + Grammar(Solver solver, long pointer) { + super(solver, pointer); + } + + protected static native void deletePointer(long pointer); + + public long getPointer() { + return pointer; + } + + @Override + public void finalize() { + deletePointer(pointer); + } + + // endregion + + /** + * Add \p rule to the set of rules corresponding to \p ntSymbol. + * @param ntSymbol the non-terminal to which the rule is added + * @param rule the rule to add + */ + public void addRule(Term ntSymbol, Term rule) { + addRule(pointer, ntSymbol.getPointer(), rule.getPointer()); + } + + private native void addRule( + long pointer, long ntSymbolPointer, long rulePointer); + + /** + * Add \p rules to the set of rules corresponding to \p ntSymbol. + * @param ntSymbol the non-terminal to which the rules are added + * @param rules the rules to add + */ + public void addRules(Term ntSymbol, Term[] rules) { + long[] pointers = Utils.getPointers(rules); + addRules(pointer, ntSymbol.getPointer(), pointers); + } + + public native void addRules( + long pointer, long ntSymbolPointer, long[] rulePointers); + + /** + * Allow \p ntSymbol to be an arbitrary constant. + * @param ntSymbol the non-terminal allowed to be any constant + */ + void addAnyConstant(Term ntSymbol) { + addAnyConstant(pointer, ntSymbol.getPointer()); + } + + private native void addAnyConstant(long pointer, long ntSymbolPointer); + + /** + * Allow \p ntSymbol to be any input variable to corresponding + * synth-fun/synth-inv with the same sort as \p ntSymbol. + * @param ntSymbol the non-terminal allowed to be any input constant + */ + void addAnyVariable(Term ntSymbol) { + addAnyVariable(pointer, ntSymbol.getPointer()); + } + + private native void addAnyVariable(long pointer, long ntSymbolPointer); + + /** + * @return a string representation of this grammar. + */ + protected native String toString(long pointer); +} diff --git a/src/api/java/jni/cvc5_Grammar.cpp b/src/api/java/jni/cvc5_Grammar.cpp new file mode 100644 index 000000000..95af2108f --- /dev/null +++ b/src/api/java/jni/cvc5_Grammar.cpp @@ -0,0 +1,120 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 Java API. + */ + +#include "cvc5_Grammar.h" + +#include "api/cpp/cvc5.h" +#include "cvc5JavaApi.h" + +using namespace cvc5::api; + +/* + * Class: cvc5_Grammar + * Method: deletePointer + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_deletePointer(JNIEnv*, + jclass, + jlong pointer) +{ + delete reinterpret_cast<Grammar*>(pointer); +} + +/* + * Class: cvc5_Grammar + * Method: addRule + * Signature: (JJJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_addRule(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer, + jlong rulePointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer); + Term* rule = reinterpret_cast<Term*>(rulePointer); + current->addRule(*ntSymbol, *rule); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Grammar + * Method: addRules + * Signature: (JJ[J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_addRules(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer, + jlongArray rulePointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer); + std::vector<Term> rules = getObjectsFromPointers<Term>(env, rulePointers); + current->addRules(*ntSymbol, rules); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Grammar + * Method: addAnyConstant + * Signature: (JJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyConstant(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer); + current->addAnyConstant(*ntSymbol); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Grammar + * Method: addAnyVariable + * Signature: (JJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyVariable(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer); + current->addAnyVariable(*ntSymbol); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Grammar + * Method: toString + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Grammar_toString(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + return env->NewStringUTF(current->toString().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index fdc1872e7..99e471b0a 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -122,6 +122,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort getSort() except + bint isNull() except + bint isIndexed() except + + size_t getNumIndices() except + T getIndices[T]() except + string toString() except + @@ -141,19 +142,23 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isEntailmentUnknown() except + bint operator==(const Result& r) except + bint operator!=(const Result& r) except + - string getUnknownExplanation() except + + UnknownExplanation getUnknownExplanation() except + string toString() except + cdef cppclass RoundingMode: pass + cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::Result": + cdef cppclass UnknownExplanation: + pass + cdef cppclass Solver: Solver(Options*) except + - bint supportsFloatingPoint() except + Sort getBooleanSort() except + Sort getIntegerSort() except + + Sort getNullSort() except + Sort getRealSort() except + Sort getRegExpSort() except + Sort getRoundingModeSort() except + @@ -179,10 +184,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkTerm(Op op, const vector[Term]& children) except + Term mkTuple(const vector[Sort]& sorts, const vector[Term]& terms) except + Op mkOp(Kind kind) except + - Op mkOp(Kind kind, Kind k) except + Op mkOp(Kind kind, const string& arg) except + Op mkOp(Kind kind, uint32_t arg) except + Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except + + Op mkOp(Kind kind, const vector[uint32_t]& args) except + # Sygus related functions Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except + Term mkSygusVar(Sort sort, const string& symbol) except + @@ -208,9 +213,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkRegexpEmpty() except + Term mkRegexpSigma() except + Term mkEmptySet(Sort s) except + + Term mkEmptyBag(Sort s) except + Term mkSepNil(Sort sort) except + Term mkString(const string& s) except + Term mkString(const wstring& s) except + + Term mkString(const string& s, bint useEscSequences) except + Term mkEmptySequence(Sort sort) except + Term mkUniverseSet(Sort sort) except + Term mkBitVector(uint32_t size) except + @@ -433,3 +440,16 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::RoundingMode": cdef RoundingMode ROUND_TOWARD_NEGATIVE, cdef RoundingMode ROUND_TOWARD_ZERO, cdef RoundingMode ROUND_NEAREST_TIES_TO_AWAY + + +cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::Result::UnknownExplanation": + cdef UnknownExplanation REQUIRES_FULL_CHECK + cdef UnknownExplanation INCOMPLETE + cdef UnknownExplanation TIMEOUT + cdef UnknownExplanation RESOURCEOUT + cdef UnknownExplanation MEMOUT + cdef UnknownExplanation INTERRUPTED + cdef UnknownExplanation NO_STATUS + cdef UnknownExplanation UNSUPPORTED + cdef UnknownExplanation OTHER + cdef UnknownExplanation UNKNOWN_REASON diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 258005207..d31fdc126 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -18,6 +18,7 @@ from cvc5 cimport DatatypeDecl as c_DatatypeDecl from cvc5 cimport DatatypeSelector as c_DatatypeSelector from cvc5 cimport Result as c_Result from cvc5 cimport RoundingMode as c_RoundingMode +from cvc5 cimport UnknownExplanation as c_UnknownExplanation from cvc5 cimport Op as c_Op from cvc5 cimport Solver as c_Solver from cvc5 cimport Grammar as c_Grammar @@ -25,6 +26,10 @@ from cvc5 cimport Sort as c_Sort from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY +from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT +from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED +from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON +from cvc5 cimport OTHER from cvc5 cimport Term as c_Term from cvc5 cimport hash as c_hash from cvc5 cimport wstring as c_wstring @@ -340,10 +345,13 @@ cdef class Op: def isNull(self): return self.cop.isNull() + def getNumIndices(self): + return self.cop.getNumIndices() + def getIndices(self): indices = None try: - indices = self.cop.getIndices[string]() + indices = self.cop.getIndices[string]().decode() except: pass @@ -418,7 +426,7 @@ cdef class Result: return self.cr != other.cr def getUnknownExplanation(self): - return self.cr.getUnknownExplanation().decode() + return UnknownExplanation(<int> self.cr.getUnknownExplanation()) def __str__(self): return self.cr.toString().decode() @@ -451,6 +459,30 @@ cdef class RoundingMode: return self.name +cdef class UnknownExplanation: + cdef c_UnknownExplanation cue + cdef str name + def __cinit__(self, int ue): + # crm always assigned externally + self.cue = <c_UnknownExplanation> ue + self.name = __unknown_explanations[ue] + + def __eq__(self, UnknownExplanation other): + return (<int> self.cue) == (<int> other.cue) + + def __ne__(self, UnknownExplanation other): + return not self.__eq__(other) + + def __hash__(self): + return hash((<int> self.crm, self.name)) + + def __str__(self): + return self.name + + def __repr__(self): + return self.name + + cdef class Solver: cdef c_Solver* csolver @@ -460,9 +492,6 @@ cdef class Solver: def __dealloc__(self): del self.csolver - def supportsFloatingPoint(self): - return self.csolver.supportsFloatingPoint() - def getBooleanSort(self): cdef Sort sort = Sort(self) sort.csort = self.csolver.getBooleanSort() @@ -473,6 +502,11 @@ cdef class Solver: sort.csort = self.csolver.getIntegerSort() return sort + def getNullSort(self): + cdef Sort sort = Sort(self) + sort.csort = self.csolver.getNullSort() + return sort + def getRealSort(self): cdef Sort sort = Sort(self) sort.csort = self.csolver.getRealSort() @@ -675,8 +709,8 @@ cdef class Solver: result.cterm = self.csolver.mkTuple(csorts, cterms) return result - - def mkOp(self, kind k, arg0=None, arg1 = None): + @expand_list_arg(num_req_args=0) + def mkOp(self, kind k, *args): ''' Supports the following uses: Op mkOp(Kind kind) @@ -686,28 +720,30 @@ cdef class Solver: Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1) ''' cdef Op op = Op(self) + cdef vector[int] v - if arg0 is None: + if len(args) == 0: op.cop = self.csolver.mkOp(k.k) - elif arg1 is None: - if isinstance(arg0, kind): - op.cop = self.csolver.mkOp(k.k, (<kind?> arg0).k) - elif isinstance(arg0, str): + elif len(args) == 1: + if isinstance(args[0], str): op.cop = self.csolver.mkOp(k.k, <const string &> - arg0.encode()) - elif isinstance(arg0, int): - op.cop = self.csolver.mkOp(k.k, <int?> arg0) + args[0].encode()) + elif isinstance(args[0], int): + op.cop = self.csolver.mkOp(k.k, <int?> args[0]) + elif isinstance(args[0], list): + for a in args[0]: + v.push_back((<int?> a)) + op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v) else: raise ValueError("Unsupported signature" - " mkOp: {}".format(" X ".join([str(k), str(arg0)]))) - else: - if isinstance(arg0, int) and isinstance(arg1, int): - op.cop = self.csolver.mkOp(k.k, <int> arg0, - <int> arg1) + " mkOp: {}".format(" X ".join([str(k), str(args[0])]))) + elif len(args) == 2: + if isinstance(args[0], int) and isinstance(args[1], int): + op.cop = self.csolver.mkOp(k.k, <int> args[0], <int> args[1]) else: raise ValueError("Unsupported signature" - " mkOp: {}".format(" X ".join([k, arg0, arg1]))) + " mkOp: {}".format(" X ".join([k, args[0], args[1]]))) return op def mkTrue(self): @@ -781,17 +817,24 @@ cdef class Solver: term.cterm = self.csolver.mkEmptySet(s.csort) return term + def mkEmptyBag(self, Sort s): + cdef Term term = Term(self) + term.cterm = self.csolver.mkEmptyBag(s.csort) + return term def mkSepNil(self, Sort sort): cdef Term term = Term(self) term.cterm = self.csolver.mkSepNil(sort.csort) return term - def mkString(self, str s): + def mkString(self, str s, useEscSequences = None): cdef Term term = Term(self) cdef Py_ssize_t size cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size) - term.cterm = self.csolver.mkString(c_wstring(tmp, size)) + if isinstance(useEscSequences, bool): + term.cterm = self.csolver.mkString(s.encode(), <bint> useEscSequences) + else: + term.cterm = self.csolver.mkString(c_wstring(tmp, size)) PyMem_Free(tmp) return term @@ -1867,3 +1910,30 @@ for rm_int, name in __rounding_modes.items(): del r del rm_int del name + + +# Generate unknown explanations +cdef __unknown_explanations = { + <int> REQUIRES_FULL_CHECK: "RequiresFullCheck", + <int> INCOMPLETE: "Incomplete", + <int> TIMEOUT: "Timeout", + <int> RESOURCEOUT: "Resourceout", + <int> MEMOUT: "Memout", + <int> INTERRUPTED: "Interrupted", + <int> NO_STATUS: "NoStatus", + <int> UNSUPPORTED: "Unsupported", + <int> OTHER: "Other", + <int> UNKNOWN_REASON: "UnknownReason" +} + +for ue_int, name in __unknown_explanations.items(): + u = UnknownExplanation(ue_int) + + if name in dir(mod_ref): + raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name) + + setattr(mod_ref, name, u) + +del u +del ue_int +del name diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 61951841b..c6b004574 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -120,25 +120,23 @@ std::string Configuration::copyright() { << "See licenses/antlr3-LICENSE for copyright and licensing information." << "\n\n"; - if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical() + ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n" + << "third party libraries.\n\n"; + + ss << " CaDiCaL - Simplified Satisfiability Solver\n" + << " See https://github.com/arminbiere/cadical for copyright " + << "information.\n\n"; + + if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCryptominisat() || Configuration::isBuiltWithKissat() - || Configuration::isBuiltWithSymFPU() || Configuration::isBuiltWithEditline()) { - ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n" - << "third party libraries.\n\n"; if (Configuration::isBuiltWithAbc()) { ss << " ABC - A System for Sequential Synthesis and Verification\n" << " See http://bitbucket.org/alanmi/abc for copyright and\n" << " licensing information.\n\n"; } - if (Configuration::isBuiltWithCadical()) - { - ss << " CaDiCaL - Simplified Satisfiability Solver\n" - << " See https://github.com/arminbiere/cadical for copyright " - << "information.\n\n"; - } if (Configuration::isBuiltWithCryptominisat()) { ss << " CryptoMiniSat - An Advanced SAT Solver\n" @@ -151,12 +149,6 @@ std::string Configuration::copyright() { << " See https://fmv.jku.at/kissat for copyright " << "information.\n\n"; } - if (Configuration::isBuiltWithSymFPU()) - { - ss << " SymFPU - The Symbolic Floating Point Unit\n" - << " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright " - << "information.\n\n"; - } if (Configuration::isBuiltWithEditline()) { ss << " Editline Library\n" @@ -165,6 +157,10 @@ std::string Configuration::copyright() { } } + ss << " SymFPU - The Symbolic Floating Point Unit\n" + << " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright " + << "information.\n\n"; + if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly()) { ss << "This version of cvc5 is linked against the following third party\n" @@ -244,8 +240,6 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } -bool Configuration::isBuiltWithCadical() { return IS_CADICAL_BUILD; } - bool Configuration::isBuiltWithCryptominisat() { return IS_CRYPTOMINISAT_BUILD; } @@ -259,8 +253,6 @@ bool Configuration::isBuiltWithPoly() return IS_POLY_BUILD; } -bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; } - unsigned Configuration::getNumDebugTags() { #if defined(CVC5_DEBUG) && defined(CVC5_TRACING) /* -1 because a NULL pointer is inserted as the last value */ diff --git a/src/base/configuration.h b/src/base/configuration.h index 78e86f920..71c79c22e 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -103,8 +103,6 @@ public: static bool isBuiltWithAbc(); - static bool isBuiltWithCadical(); - static bool isBuiltWithCryptominisat(); static bool isBuiltWithKissat(); @@ -113,8 +111,6 @@ public: static bool isBuiltWithPoly(); - static bool isBuiltWithSymFPU(); - /* Return the number of debug tags */ static unsigned getNumDebugTags(); /* Return a sorted array of the debug tags name */ diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 3027b23bc..b348da380 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -96,12 +96,6 @@ namespace cvc5 { # define IS_ABC_BUILD false #endif /* CVC5_USE_ABC */ -#if CVC5_USE_CADICAL -#define IS_CADICAL_BUILD true -#else /* CVC5_USE_CADICAL */ -#define IS_CADICAL_BUILD false -#endif /* CVC5_USE_CADICAL */ - #if CVC5_USE_CRYPTOMINISAT # define IS_CRYPTOMINISAT_BUILD true #else /* CVC5_USE_CRYPTOMINISAT */ @@ -126,12 +120,6 @@ namespace cvc5 { #define IS_EDITLINE_BUILD false #endif /* HAVE_LIBEDITLINE */ -#ifdef CVC5_USE_SYMFPU -#define IS_SYMFPU_BUILD true -#else /* HAVE_SYMFPU_HEADERS */ -#define IS_SYMFPU_BUILD false -#endif /* HAVE_SYMFPU_HEADERS */ - #if CVC5_GPL_DEPS # define IS_GPL_BUILD true #else /* CVC5_GPL_DEPS */ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index b58cd45a9..e41b63191 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -38,14 +38,13 @@ namespace attr { /** * Attributes are roughly speaking [almost] global hash tables from Nodes * (TNodes) to data. Attributes can be thought of as additional fields used to - * extend NodeValues. Attributes are mutable and come in both sat - * context-dependent and non-context dependent varieties. Attributes live only - * as long as the node itself does. If a Node is garbage-collected, Attributes - * associated with it will automatically be garbage collected. (Being in the - * domain of an Attribute does not increase a Node's reference count.) To - * achieve this special relationship with Nodes, Attributes are mapped by hash - * tables (AttrHash<> and CDAttrHash<>) that live in the AttributeManager. The - * AttributeManager is owned by the NodeManager. + * extend NodeValues. Attributes are mutable. Attributes live only as long as + * the node itself does. If a Node is garbage-collected, Attributes associated + * with it will automatically be garbage collected. (Being in the domain of an + * Attribute does not increase a Node's reference count.) To achieve this + * special relationship with Nodes, Attributes are mapped by hash tables + * (AttrHash<>) that live in the AttributeManager. The AttributeManager is + * owned by the NodeManager. * * Example: * @@ -67,11 +66,11 @@ namespace attr { * ``` * * To separate Attributes of the same type in the same table, each of the - * structures `struct InstLevelAttributeId {};` is given a different unique value - * at load time. An example is the empty struct InstLevelAttributeId. These - * should be unique for each Attribute. Then via some template messiness when - * InstLevelAttribute() is passed as the argument to getAttribute(...) the load - * time id is instantiated. + * structures `struct InstLevelAttributeId {};` is given a different unique + * value at load time. An example is the empty struct InstLevelAttributeId. + * These should be unique for each Attribute. Then via some template messiness + * when InstLevelAttribute() is passed as the argument to getAttribute(...) the + * load time id is instantiated. */ // ATTRIBUTE MANAGER =========================================================== @@ -97,7 +96,7 @@ class AttributeManager { * getTable<> is a helper template that gets the right table from an * AttributeManager given its type. */ - template <class T, bool context_dep, class Enable> + template <class T, class Enable> friend struct getTable; bool d_inGarbageCollection; @@ -232,12 +231,13 @@ namespace attr { * `std::enable_if` in the template parameter and the condition is false), the * instantiation is ignored due to the SFINAE rule. */ -template <class T, bool context_dep, class Enable = void> +template <class T, class Enable = void> struct getTable; /** Access the "d_bools" member of AttributeManager. */ template <> -struct getTable<bool, false> { +struct getTable<bool> +{ static const AttrTableId id = AttrTableBool; typedef AttrHash<bool> table_type; static inline table_type& get(AttributeManager& am) { @@ -251,7 +251,6 @@ struct getTable<bool, false> { /** Access the "d_ints" member of AttributeManager. */ template <class T> struct getTable<T, - false, // Use this specialization only for unsigned integers typename std::enable_if<std::is_unsigned<T>::value>::type> { @@ -267,7 +266,8 @@ struct getTable<T, /** Access the "d_tnodes" member of AttributeManager. */ template <> -struct getTable<TNode, false> { +struct getTable<TNode> +{ static const AttrTableId id = AttrTableTNode; typedef AttrHash<TNode> table_type; static inline table_type& get(AttributeManager& am) { @@ -280,7 +280,8 @@ struct getTable<TNode, false> { /** Access the "d_nodes" member of AttributeManager. */ template <> -struct getTable<Node, false> { +struct getTable<Node> +{ static const AttrTableId id = AttrTableNode; typedef AttrHash<Node> table_type; static inline table_type& get(AttributeManager& am) { @@ -293,7 +294,8 @@ struct getTable<Node, false> { /** Access the "d_types" member of AttributeManager. */ template <> -struct getTable<TypeNode, false> { +struct getTable<TypeNode> +{ static const AttrTableId id = AttrTableTypeNode; typedef AttrHash<TypeNode> table_type; static inline table_type& get(AttributeManager& am) { @@ -306,7 +308,8 @@ struct getTable<TypeNode, false> { /** Access the "d_strings" member of AttributeManager. */ template <> -struct getTable<std::string, false> { +struct getTable<std::string> +{ static const AttrTableId id = AttrTableString; typedef AttrHash<std::string> table_type; static inline table_type& get(AttributeManager& am) { @@ -329,11 +332,9 @@ typename AttrKind::value_type AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>:: - table_type table_type; + typedef typename getTable<value_type>::table_type table_type; - const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this); + const table_type& ah = getTable<value_type>::get(*this); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -371,12 +372,9 @@ struct HasAttribute<true, AttrKind> { typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, - AttrKind::context_dependent>::table_type - table_type; + typedef typename getTable<value_type>::table_type table_type; - const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am); + const table_type& ah = getTable<value_type>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -400,11 +398,9 @@ struct HasAttribute<false, AttrKind> { NodeValue* nv) { typedef typename AttrKind::value_type value_type; //typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>:: - table_type table_type; + typedef typename getTable<value_type>::table_type table_type; - const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am); + const table_type& ah = getTable<value_type>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -420,11 +416,9 @@ struct HasAttribute<false, AttrKind> { typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>:: - table_type table_type; + typedef typename getTable<value_type>::table_type table_type; - const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am); + const table_type& ah = getTable<value_type>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -460,11 +454,9 @@ AttributeManager::setAttribute(NodeValue* nv, const typename AttrKind::value_type& value) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type, AttrKind::context_dependent>:: - table_type table_type; + typedef typename getTable<value_type>::table_type table_type; - table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this); + table_type& ah = getTable<value_type>::get(*this); ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } @@ -473,7 +465,7 @@ template <class T> inline void AttributeManager::deleteFromTable(AttrHash<T>& table, NodeValue* nv) { // This cannot use nv as anything other than a pointer! - const uint64_t last = attr::LastAttributeId<T, false>::getId(); + const uint64_t last = attr::LastAttributeId<T>::getId(); for (uint64_t id = 0; id < last; ++id) { table.erase(std::make_pair(id, nv)); @@ -493,8 +485,7 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { template <class AttrKind> AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){ typedef typename AttrKind::value_type value_type; - AttrTableId tableId = getTable<value_type, - AttrKind::context_dependent>::id; + AttrTableId tableId = getTable<value_type>::id; return AttributeUniqueId(tableId, attr.getId()); } diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index c82e62836..2ae216d3c 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -372,8 +372,9 @@ namespace attr { * This is the last-attribute-assigner. IDs are not globally * unique; rather, they are unique for each table_value_type. */ -template <class T, bool context_dep> -struct LastAttributeId { +template <class T> +struct LastAttributeId +{ public: static uint64_t getNextId() { uint64_t* id = raw_id(); @@ -402,11 +403,8 @@ struct LastAttributeId { * @param T the tag for the attribute kind. * * @param value_t the underlying value_type for the attribute kind - * - * @param context_dep whether this attribute kind is - * context-dependent */ -template <class T, class value_t, bool context_dep = false> +template <class T, class value_t> class Attribute { /** @@ -432,11 +430,6 @@ public: static const bool has_default_value = false; /** - * Expose this setting to the users of this Attribute kind. - */ - static const bool context_dependent = context_dep; - - /** * Register this attribute kind and check that the ID is a valid ID * for bool-valued attributes. Fail an assert if not. Otherwise * return the id. @@ -444,15 +437,15 @@ public: static inline uint64_t registerAttribute() { typedef typename attr::KindValueToTableValueMapping<value_t>:: table_value_type table_value_type; - return attr::LastAttributeId<table_value_type, context_dep>::getNextId(); + return attr::LastAttributeId<table_value_type>::getNextId(); } };/* class Attribute<> */ /** * An "attribute type" structure for boolean flags (special). */ -template <class T, bool context_dep> -class Attribute<T, bool, context_dep> +template <class T> +class Attribute<T, bool> { /** IDs for bool-valued attributes are actually bit assignments. */ static const uint64_t s_id; @@ -480,17 +473,12 @@ public: static const bool default_value = false; /** - * Expose this setting to the users of this Attribute kind. - */ - static const bool context_dependent = context_dep; - - /** * Register this attribute kind and check that the ID is a valid ID * for bool-valued attributes. Fail an assert if not. Otherwise * return the id. */ static inline uint64_t registerAttribute() { - const uint64_t id = attr::LastAttributeId<bool, context_dep>::getNextId(); + const uint64_t id = attr::LastAttributeId<bool>::getNextId(); AlwaysAssert(id <= 63) << "Too many boolean node attributes registered " "during initialization !"; return id; @@ -500,15 +488,14 @@ public: // ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= /** Assign unique IDs to attributes at load time. */ -template <class T, class value_t, bool context_dep> -const uint64_t Attribute<T, value_t, context_dep>::s_id = - Attribute<T, value_t, context_dep>::registerAttribute(); - +template <class T, class value_t> +const uint64_t Attribute<T, value_t>::s_id = + Attribute<T, value_t>::registerAttribute(); /** Assign unique IDs to attributes at load time. */ -template <class T, bool context_dep> -const uint64_t Attribute<T, bool, context_dep>::s_id = - Attribute<T, bool, context_dep>::registerAttribute(); +template <class T> +const uint64_t Attribute<T, bool>::s_id = + Attribute<T, bool>::registerAttribute(); } // namespace expr } // namespace cvc5 diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 6bdc1abc9..b6ead1b70 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -26,7 +26,8 @@ #include <vector> #include "main/main.h" -#include "options/options_public.h" +#include "options/base_options.h" +#include "options/main_options.h" #include "smt/command.h" #include "smt/smt_engine.h" @@ -65,7 +66,7 @@ CommandExecutor::~CommandExecutor() void CommandExecutor::printStatistics(std::ostream& out) const { - if (options::getStatistics(d_options)) + if (d_options.base.statistics) { getSmtEngine()->printStatistics(out); } @@ -73,7 +74,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const void CommandExecutor::printStatisticsSafe(int fd) const { - if (options::getStatistics(d_options)) + if (d_options.base.statistics) { getSmtEngine()->printStatisticsSafe(fd); } @@ -81,7 +82,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const bool CommandExecutor::doCommand(Command* cmd) { - if (options::getParseOnly(d_options)) + if (d_options.base.parseOnly) { return true; } @@ -100,9 +101,9 @@ bool CommandExecutor::doCommand(Command* cmd) return status; } else { - if (options::getVerbosity(d_options) > 2) + if (d_options.base.verbosity > 2) { - *options::getOut(d_options) << "Invoking: " << *cmd << std::endl; + *d_options.base.out << "Invoking: " << *cmd << std::endl; } return doCommandSingleton(cmd); @@ -111,7 +112,7 @@ bool CommandExecutor::doCommand(Command* cmd) void CommandExecutor::reset() { - printStatistics(*options::getErr(d_options)); + printStatistics(*d_options.base.err); /* We have to keep options passed via CL on reset. These options are stored * in CommandExecutor::d_options (populated and created in the driver), and * CommandExecutor::d_options only contains *these* options since the @@ -124,10 +125,10 @@ void CommandExecutor::reset() bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; - if (options::getVerbosity(d_options) >= -1) + if (d_options.base.verbosity >= -1) { status = solverInvoke( - d_solver.get(), d_symman.get(), cmd, options::getOut(d_options)); + d_solver.get(), d_symman.get(), cmd, d_options.base.out); } else { @@ -150,9 +151,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) d_result = res = q->getResult(); } - if ((cs != nullptr || q != nullptr) && options::getStatsEveryQuery(d_options)) + if ((cs != nullptr || q != nullptr) && d_options.base.statisticsEveryQuery) { - getSmtEngine()->printStatisticsDiff(*options::getErr(d_options)); + getSmtEngine()->printStatisticsDiff(*d_options.base.err); } bool isResultUnsat = res.isUnsat() || res.isEntailed(); @@ -160,32 +161,32 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) // dump the model/proof/unsat core if option is set if (status) { std::vector<std::unique_ptr<Command> > getterCommands; - if (options::getDumpModels(d_options) + if (d_options.driver.dumpModels && (res.isSat() || (res.isSatUnknown() && res.getUnknownExplanation() == api::Result::INCOMPLETE))) { getterCommands.emplace_back(new GetModelCommand()); } - if (options::getDumpProofs(d_options) && isResultUnsat) + if (d_options.driver.dumpProofs && isResultUnsat) { getterCommands.emplace_back(new GetProofCommand()); } - if (options::getDumpInstantiations(d_options) + if (d_options.driver.dumpInstantiations && GetInstantiationsCommand::isEnabled(d_solver.get(), res)) { getterCommands.emplace_back(new GetInstantiationsCommand()); } - if (options::getDumpUnsatCores(d_options) && isResultUnsat) + if ((d_options.driver.dumpUnsatCores || d_options.driver.dumpUnsatCoresFull) && isResultUnsat) { getterCommands.emplace_back(new GetUnsatCoreCommand()); } if (!getterCommands.empty()) { // set no time limit during dumping if applicable - if (options::getForceNoLimitCpuWhileDump(d_options)) + if (d_options.driver.forceNoLimitCpuWhileDump) { setNoLimitCPU(); } @@ -225,17 +226,17 @@ bool solverInvoke(api::Solver* solver, } void CommandExecutor::flushOutputStreams() { - printStatistics(*(options::getErr(d_options))); + printStatistics(*d_options.base.err); // make sure out and err streams are flushed too - if (options::getOut(d_options) != nullptr) + if (d_options.base.out != nullptr) { - *options::getOut(d_options) << std::flush; + *d_options.base.out << std::flush; } - if (options::getErr(d_options) != nullptr) + if (d_options.base.err != nullptr) { - *options::getErr(d_options) << std::flush; + *d_options.base.err << std::flush; } } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 75c7b2a01..2bc5c59f3 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -33,8 +33,9 @@ #include "main/main.h" #include "main/signal_handlers.h" #include "main/time_limit.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/options_public.h" +#include "options/parser_options.h" #include "options/main_options.h" #include "options/set_language.h" #include "parser/parser.h" @@ -88,9 +89,9 @@ void printUsage(Options& opts, bool full) { << endl << "cvc5 options:" << endl; if(full) { - Options::printUsage(ss.str(), *(options::getOut(opts))); + Options::printUsage(ss.str(), *opts.base.out); } else { - Options::printShortUsage(ss.str(), *(options::getOut(opts))); + Options::printShortUsage(ss.str(), *opts.base.out); } } @@ -116,14 +117,14 @@ int runCvc5(int argc, char* argv[], Options& opts) printUsage(opts, true); exit(1); } - else if (options::getLanguageHelp(opts)) + else if (opts.base.languageHelp) { - Options::printLanguageHelp(*(options::getOut(opts))); + Options::printLanguageHelp(*opts.base.out); exit(1); } else if (opts.driver.version) { - *(options::getOut(opts)) << Configuration::about().c_str() << flush; + *opts.base.out << Configuration::about().c_str() << flush; exit(0); } @@ -131,7 +132,7 @@ int runCvc5(int argc, char* argv[], Options& opts) // If in competition mode, set output stream option to flush immediately #ifdef CVC5_COMPETITION_MODE - *(options::getOut(opts)) << unitbuf; + *opts.base.out << unitbuf; #endif /* CVC5_COMPETITION_MODE */ // We only accept one input file @@ -143,7 +144,7 @@ int runCvc5(int argc, char* argv[], Options& opts) const bool inputFromStdin = filenames.empty() || filenames[0] == "-"; // if we're reading from stdin on a TTY, default to interactive mode - if (!options::wasSetByUserInteractive(opts)) + if (!opts.driver.interactiveWasSetByUser) { opts.driver.interactive = inputFromStdin && isatty(fileno(stdin)); } @@ -157,33 +158,32 @@ int runCvc5(int argc, char* argv[], Options& opts) } const char* filename = filenameStr.c_str(); - if (options::getInputLanguage(opts) == language::input::LANG_AUTO) + if (opts.base.inputLanguage == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - options::setInputLanguage(language::input::LANG_CVC, opts); + opts.base.inputLanguage = language::input::LANG_CVC; } else { size_t len = filenameStr.size(); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - options::setInputLanguage(language::input::LANG_SMTLIB_V2_6, opts); + opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - options::setInputLanguage(language::input::LANG_TPTP, opts); + opts.base.inputLanguage = language::input::LANG_TPTP; } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - options::setInputLanguage(language::input::LANG_CVC, opts); + opts.base.inputLanguage = language::input::LANG_CVC; } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { // version 2 sygus is the default - options::setInputLanguage(language::input::LANG_SYGUS_V2, opts); + opts.base.inputLanguage = language::input::LANG_SYGUS_V2; } } } - if (options::getOutputLanguage(opts) == language::output::LANG_AUTO) + if (opts.base.outputLanguage == language::output::LANG_AUTO) { - options::setOutputLanguage( - language::toOutputLanguage(options::getInputLanguage(opts)), opts); + opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage); } // Determine which messages to show based on smtcomp_mode and verbosity @@ -197,8 +197,8 @@ int runCvc5(int argc, char* argv[], Options& opts) } // important even for muzzled builds (to get result output right) - (*(options::getOut(opts))) - << language::SetLanguage(options::getOutputLanguage(opts)); + (*opts.base.out) + << language::SetLanguage(opts.base.outputLanguage); // Create the command executor to execute the parsed commands pExecutor = std::make_unique<CommandExecutor>(opts); @@ -213,7 +213,7 @@ int runCvc5(int argc, char* argv[], Options& opts) bool status = true; if (opts.driver.interactive && inputFromStdin) { - if (!options::wasSetByUserIncrementalSolving(opts)) + if (!opts.base.incrementalSolvingWasSetByUser) { cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); @@ -240,7 +240,7 @@ int runCvc5(int argc, char* argv[], Options& opts) try { cmd.reset(shell.readCommand()); } catch(UnsafeInterruptException& e) { - (*options::getOut(opts)) << CommandInterrupted(); + *opts.base.out << CommandInterrupted(); break; } if (cmd == nullptr) @@ -253,7 +253,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } else { - if (!options::wasSetByUserIncrementalSolving(opts)) + if (!opts.base.incrementalSolvingWasSetByUser) { cmd.reset(new SetOptionCommand("incremental", "false")); cmd->setMuted(true); @@ -266,20 +266,20 @@ int runCvc5(int argc, char* argv[], Options& opts) std::unique_ptr<Parser> parser(parserBuilder.build()); if( inputFromStdin ) { parser->setInput(Input::newStreamInput( - options::getInputLanguage(opts), cin, filename)); + opts.base.inputLanguage, cin, filename)); } else { - parser->setInput(Input::newFileInput(options::getInputLanguage(opts), + parser->setInput(Input::newFileInput(opts.base.inputLanguage, filename, - options::getMemoryMap(opts))); + opts.parser.memoryMap)); } bool interrupted = false; while (status) { if (interrupted) { - (*options::getOut(opts)) << CommandInterrupted(); + *opts.base.out << CommandInterrupted(); pExecutor->reset(); break; } @@ -313,9 +313,9 @@ int runCvc5(int argc, char* argv[], Options& opts) } #ifdef CVC5_COMPETITION_MODE - if (cvc5::options::getOut(opts) != nullptr) + if (opts.base.out != nullptr) { - *cvc5::options::getOut(opts) << std::flush; + *opts.base.out << std::flush; } // exit, don't return (don't want destructors to run) // _exit() from unistd.h doesn't run global destructors @@ -327,7 +327,7 @@ int runCvc5(int argc, char* argv[], Options& opts) pExecutor->flushOutputStreams(); #ifdef CVC5_DEBUG - if (opts.driver.earlyExit && options::wasSetByUserEarlyExit(opts)) + if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser) { _exit(returnValue); } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 048c101f0..964b88ea0 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -40,10 +40,11 @@ #include "base/check.h" #include "base/output.h" #include "expr/symbol_manager.h" +#include "options/base_options.h" #include "options/language.h" #include "options/main_options.h" #include "options/options.h" -#include "options/options_public.h" +#include "options/parser_options.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -89,16 +90,16 @@ static set<string> s_declarations; InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) : d_options(solver->getOptions()), - d_in(*options::getIn(d_options)), - d_out(*options::getOut(d_options)), + d_in(*d_options.base.in), + d_out(*d_options.base.out), d_quit(false) { ParserBuilder parserBuilder(solver, sm, d_options); /* Create parser with bogus input. */ d_parser = parserBuilder.build(); - if (options::wasSetByUserForceLogicString(d_options)) + if (d_options.parser.forceLogicStringWasSetByUser) { - LogicInfo tmp(options::getForceLogicString(d_options)); + LogicInfo tmp(d_options.parser.forceLogicString); d_parser->forceLogic(tmp.getLogicString()); } @@ -113,7 +114,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) ::using_history(); OutputLanguage lang = - toOutputLanguage(options::getInputLanguage(d_options)); + toOutputLanguage(d_options.base.inputLanguage); switch(lang) { case output::LANG_CVC: d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; @@ -314,7 +315,7 @@ restart: } d_parser->setInput(Input::newStringInput( - options::getInputLanguage(d_options), input, INPUT_FILENAME)); + d_options.base.inputLanguage, input, INPUT_FILENAME)); /* There may be more than one command in the input. Build up a sequence. */ @@ -365,7 +366,7 @@ restart: } catch (ParserException& pe) { - if (language::isOutputLang_smt2(options::getOutputLanguage(d_options))) + if (language::isOutputLang_smt2(d_options.base.outputLanguage)) { d_out << "(error \"" << pe << "\")" << endl; } diff --git a/src/main/main.cpp b/src/main/main.cpp index 2b25e6c93..a00e29b04 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -26,10 +26,10 @@ #include "base/output.h" #include "main/command_executor.h" #include "main/interactive_shell.h" +#include "options/base_options.h" #include "options/language.h" #include "options/option_exception.h" #include "options/options.h" -#include "options/options_public.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" @@ -53,25 +53,25 @@ int main(int argc, char* argv[]) { return runCvc5(argc, argv, opts); } catch(OptionException& e) { #ifdef CVC5_COMPETITION_MODE - *options::getOut(opts) << "unknown" << endl; + *opts.base.out << "unknown" << endl; #endif cerr << "(error \"" << e << "\")" << endl << endl << "Please use --help to get help on command-line options." << endl; } catch(Exception& e) { #ifdef CVC5_COMPETITION_MODE - *options::getOut(opts) << "unknown" << endl; + *opts.base.out << "unknown" << endl; #endif - if (language::isOutputLang_smt2(options::getOutputLanguage(opts))) + if (language::isOutputLang_smt2(opts.base.outputLanguage)) { - *options::getOut(opts) << "(error \"" << e << "\")" << endl; + *opts.base.out << "(error \"" << e << "\")" << endl; } else { - *options::getErr(opts) << "(error \"" << e << "\")" << endl; + *opts.base.err << "(error \"" << e << "\")" << endl; } - if (options::getStatistics(opts) && pExecutor != nullptr) + if (opts.base.statistics && pExecutor != nullptr) { totalTime.reset(); - pExecutor->printStatistics(*options::getErr(opts)); + pExecutor->printStatistics(*opts.base.err); } } exit(1); diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index c0fc6846a..28a0087bb 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -56,7 +56,7 @@ #include <cstring> #include "base/exception.h" -#include "options/options_public.h" +#include "options/base_options.h" #include "signal_handlers.h" namespace cvc5 { @@ -80,7 +80,7 @@ TimeLimit::~TimeLimit() TimeLimit install_time_limit(const Options& opts) { - unsigned long ms = options::getCumulativeTimeLimit(opts); + uint64_t ms = opts.base.cumulativeMillisecondLimit; // Skip if no time limit shall be set. if (ms == 0) { return TimeLimit(); diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index bce6c9b6d..01cb6da42 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -53,15 +53,13 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); - } - + // the last result that is SAT + Result lastSatResult = intermediateSatResult; // value equals to upperBound value = optChecker->getValue(target); @@ -104,39 +102,35 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, nm->mkNode(LTOperator, target, nm->mkConst(pivot)))); } intermediateSatResult = optChecker->checkSat(); - if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::SAT) + switch (intermediateSatResult.isSat()) { - value = optChecker->getValue(target); - upperBound = value.getConst<BitVector>(); - } - else if (intermediateSatResult.isSat() == Result::UNSAT) - { - if (lowerBound == pivot) - { - // lowerBound == pivot ==> upperbound = lowerbound + 1 - // and lowerbound <= target < upperbound is UNSAT - // return the upperbound + case Result::SAT_UNKNOWN: optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); - } - else - { - lowerBound = pivot; - } - } - else - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); + case Result::SAT: + lastSatResult = intermediateSatResult; + value = optChecker->getValue(target); + upperBound = value.getConst<BitVector>(); + break; + case Result::UNSAT: + if (lowerBound == pivot) + { + // lowerBound == pivot ==> upperbound = lowerbound + 1 + // and lowerbound <= target < upperbound is UNSAT + // return the upperbound + optChecker->pop(); + return OptimizationResult(lastSatResult, value); + } + else + { + lowerBound = pivot; + } + break; + default: Unreachable(); } optChecker->pop(); } - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, @@ -148,15 +142,13 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); - } - + // the last result that is SAT + Result lastSatResult = intermediateSatResult; // value equals to upperBound value = optChecker->getValue(target); @@ -196,39 +188,35 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, nm->mkNode(GTOperator, target, nm->mkConst(pivot)), nm->mkNode(LEOperator, target, nm->mkConst(upperBound)))); intermediateSatResult = optChecker->checkSat(); - if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::SAT) + switch (intermediateSatResult.isSat()) { - value = optChecker->getValue(target); - lowerBound = value.getConst<BitVector>(); - } - else if (intermediateSatResult.isSat() == Result::UNSAT) - { - if (lowerBound == pivot) - { - // upperbound = lowerbound + 1 - // and lowerbound < target <= upperbound is UNSAT - // return the lowerbound + case Result::SAT_UNKNOWN: optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); - } - else - { - upperBound = pivot; - } - } - else - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); + case Result::SAT: + lastSatResult = intermediateSatResult; + value = optChecker->getValue(target); + lowerBound = value.getConst<BitVector>(); + break; + case Result::UNSAT: + if (lowerBound == pivot) + { + // upperbound = lowerbound + 1 + // and lowerbound < target <= upperbound is UNSAT + // return the lowerbound + optChecker->pop(); + return OptimizationResult(lastSatResult, value); + } + else + { + upperBound = pivot; + } + break; + default: Unreachable(); } optChecker->pop(); } - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } } // namespace cvc5::omt diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index 045268337..379b0cd43 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -33,13 +33,10 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); + return OptimizationResult(intermediateSatResult, value); } // node storing target > old_value (used in optimization loop) Node increment; @@ -56,12 +53,14 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, // then assert optimization_target > current_model_value incrementalOperator = kind::GT; } + Result lastSatResult = intermediateSatResult; // Workhorse of linear search: // This loop will keep incrmenting/decrementing the objective until unsat // When unsat is hit, // the optimized value is the model value just before the unsat call while (intermediateSatResult.isSat() == Result::SAT) { + lastSatResult = intermediateSatResult; value = optChecker->getValue(target); Assert(!value.isNull()); increment = nm->mkNode(incrementalOperator, target, value); @@ -69,7 +68,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, intermediateSatResult = optChecker->checkSat(); } optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker, diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 978c32888..cc7b621a8 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -17,7 +17,6 @@ check_python_module("toml") libcvc5_add_sources( - base_handlers.h decision_weight.h didyoumean.cpp didyoumean.h @@ -55,7 +54,6 @@ set(options_toml_files proof_options.toml prop_options.toml quantifiers_options.toml - resource_manager_options.toml sep_options.toml sets_options.toml smt_options.toml diff --git a/src/options/README b/src/options/README deleted file mode 100644 index 868690b85..000000000 --- a/src/options/README +++ /dev/null @@ -1,127 +0,0 @@ -Modules -======= - - Each options module starts with the following required attributes: - - id ... (string) ID of the module (e.g., "ARITH") - name ... (string) name of the module (e.g., "Arithmetic Theory") - header ... (string) name of the options header to generated (e.g., "options/arith_options.h") - - A module defines 0 or more options. - - In general, each attribute/value pair is required to be in one line. - Comments start with # and are not allowed in attribute/value lines. - - -Options -======= - - Options can be defined with the [[option]] tag, the required attributes for - an option are: - - category ... (string) common | expert | regular | undocumented - type ... (string) C++ type of the option value - - Optional attributes are: - - name ... (string) option name that is used to access via - options::<name>() - smt_name ... (string) alternative name to access option via - set-option/get-option commands - short ... (string) short option name consisting of one character - (no '-' prefix required) - long ... (string) long option name (required if short is specified, - no '--' prefix required). - long option names may have a suffix '=XXX' where - 'XXX' can be used to indicate the type of the - option value, e.g., '=MODE', '=LANG', '=N', ... - default ... (string) default value of type 'type' - handler ... (string) handler for parsing option values before setting - option - predicates ... (list) functions that check whether given option value is - valid - includes ... (list) header files required by handler/predicates - alternate ... (bool) true (default): add --no-<long> alternative option - false: omit --no-<long> alternative option - help ... (string) documentation (required if category is not - undocumented) - - Note that if an option defines a long option name with type 'bool', - mkoptions.py automatically generates a --no-<long> option to set the option - to false. - This behaviour can be explicitely disabled for options with attribute - alternate = false. - More information on how to use handler and predicates can be found - at the end of the README. - - - Example: - - [[option]] - name = "outputLanguage" - smt_name = "output-language" - category = "common" - short = "" - long = "output-lang=LANG" - type = "OutputLanguage" - default = "language::output::LANG_AUTO" - handler = "stringToOutputLanguage" - predicates = [] - includes = ["options/language.h"] - help = "force output language (default is \"auto\"; see --output-lang help)" - - -Further information (the old option package) -============================================ - - The options/ package supports a wide range of operations for responding to - an option being set. Roughly the three major concepts are: - - - handler to parse an option before setting its value. - - predicates to reject bad values for the option. - - More details on each class of custom handlers. - - - handler = "" - - Handlers provide support for parsing custom option types. - The signature for a handler call is: - - T custom-option-handler(std::string option, std::string optarg, - OptionsHandler* handler); - - where T is the type of the option. The suggested implementation is to - implement custom-handler as a dispatch into a function on handler with the - signature: - - T OptionsHandler::custom-option-handler(std::string option, - std::string optarg); - - The handlers are run before predicates. - Having multiple handlers is considered bad practice and is unsupported. - Handlers may have arbitrary side effects, but should call no code - inaccessible to liboptions. For side effects that are not required in order - to parse the option, using :predicate is recommended. Memory - management done by a handler needs to either be encapsulated by the type - and the destructor for the type or should *always* be owned by handler. - More elaborate memory management schemes are not currently supported. - - - predicates = [...] - - Predicates provide support for checking whether or not the value of an - option is acceptable. Predicates are run after handlers. - The signature for a predicate call is: - - void custom-predicate(std::string option, T value, - OptionsHandler* handler); - - where T is the type of the option. The suggested implementation is to - implement custom-predicate as a dispatch into a function on handler with - the signature: - - void OptionsHandler::custom-predicate(std::string option, T value); - - The predicates are run after handlers. Multiple - predicates may be defined for the same option, but the order they are run - is not guaranteed. Predicates may have arbitrary side effects, but should - call no code inaccessible to liboptions. diff --git a/src/options/README.md b/src/options/README.md new file mode 100644 index 000000000..df5686abc --- /dev/null +++ b/src/options/README.md @@ -0,0 +1,211 @@ +Specifying Modules +================== + +Every options module, that is a group of options that belong together in some +way, is declared in its own file in `options/{module name}_options.toml`. Each +options module starts with the following required attributes: + +* `id` (string): ID of the module (e.g., `"arith"`) +* `name` (string): name of the module (e.g., `"Arithmetic Theory"`) + +Additional, a module can optionally be defined to be public. A public module +includes `cvc5_public.h` instead of `cvc5_private.h` can thus be included from +"external" code like the parser or the main driver. + +* `public` (bool): make option module public + +A module defines 0 or more options. + +In general, each attribute/value pair is required to be in one line. Comments +start with # and are not allowed in attribute/value lines. + +After parsing, a module is extended to have the following attributes: + +* `id`: lower-case version of the parsed `id` +* `id_cap`: upper-case version of `id` (used for the `Holder{id_cap}` class) +* `filename`: base filename for generated files (`"{id}_options"`) +* `header`: generated header name (`"options/{filename}.h"`) + + +Specifying Options +================== + +Options can be defined within a module file with the `[[option]]` tag, the +required attributes for an option are: + +* `category` (string): one of `common`, `expert`, `regular`, or `undocumented` +* `type` (string): the C++ type of the option value + +Optional attributes are: + +* `name` (string): the option name used to access the option internally + (`d_option.{module.id}.{name}`) +* `long` (string): long option name (without `--` prefix). Long option names may + have a suffix `=XXX` where `XXX` can be used to indicate the type of the + option value, e.g., `=MODE`, `=LANG`, `=N`, ... +* `short` (string): short option name consisting of one character (no `-` prefix + required), can be given if `long` is specified +* `alias` (list): alternative names that can be used instead of `long` +* `default` (string): default value, needs to be a valid C++ expression of type + `type` +* `alternate` (bool, default `true`): if `true`, adds `--no-{long}` alternative + option +* `mode` (list): used to define options whose type shall be an auto-generated + enum, more details below +* `handler` (string): alternate parsing routine for option types not covered by + the default parsers, more details below +* `predicates` (list): custom validation function to check whether an option + value is valid, more details below +* `includes` (list): additional header files required by handler or predicate + functions +* `help` (string): documentation string (required, unless the `category` is + `undocumented`) +* `help_mode` (string): documentation for the mode enum (required if `mode` is + given) + + +Handler functions +----------------- + +Custom handler functions are used to turn the option value from a `std::string` +into the type specified by `type`. Standard handler functions are provided for +basic types (`std::string`, `bool`, integer types and floating point types) as +well as enums specified by `mode`. A custom handler function needs to be member +function of `options::OptionsHandler` with signature `{type} {handler}(const +std::string& option, const std::string& flag, const std::string& optionvalue)`, +or alternatively `void {handler}(const std::string& option, const std::string& +flag)` if the `type` is `void`. The two parameters `option` and `flag` hold the +canonical and the actually used option names, respectively, and they may differ +if an alternative name (from `alias`) was used. While `option` should be used to +identify an option (e.g. by comparing against `*__name`), `flag` should be +usually used in user messages. + + +Predicate functions +------------------- + +Predicate functions are used to check whether an option value is valid after it +has been parsed by a (standard or custom) handler function. Like a handler +function, a predicate function needs to be a member function of +`options::OptionsHandler` with signature `void {predicate}(const std::string& +option, const std::string& flag, {type} value)`. If the check fails, the +predicate should raise an `OptionException`. + + +Mode options +------------ + +An option can be defined to hold one of a given set of values we call modes. +Doing so automatically defines an `enum class` for the set of modes and makes +the option accept one of the values from the enum. The enum class will be called +`{type}` and methods `operator<<` and `stringTo{enum}` are automatically +generated. A mode is defined by specifying `[[option.mode.{NAME}]]` after the +main `[[option]]` section with the following attributes: + +* `name` (string): the string value that corresponds to the enum value +* `help` (string): documentation about this mode + +Example: + + [[option]] + name = "bitblastMode" + category = "regular" + long = "bitblast=MODE" + type = "BitblastMode" + default = "LAZY" + help = "choose bitblasting mode, see --bitblast=help" + help_mode = "Bit-blasting modes." + [[option.mode.LAZY]] + name = "lazy" + help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver." + [[option.mode.EAGER]] + name = "eager" + help = "Bitblast eagerly to bit-vector SAT solver." + +The option can now be set with `--bitblast=lazy`, `(set-option :bitblast +eager)`, or `options::set("bitblast", "eager")`. + + +Generated code +============== + +The entire options setup heavily relies on generating a lot of code from the +information retrieved from the `*_options.toml` files. After code generation, +files related to options live either in `src/options/` (if not changed) or in +`build/src/options/` (if automatically generated). After all code has been +generated, the entire options setup consists of the following components: + +* `options.h`: core `Options` class +* `options_api.h`: utility methods used by the API (`parse()`, `set()`, `get()`, + ...) +* `options_public.h`: utility methods used to access options from outside of + libcvc5 +* `{module}_options.h`: specifics for one single options module + + +`Options` class +--------------- + +The `Options` class is the central entry point for regular usage of options. It +holds a `std::unique_ptr` to an "option holder" for every option module, that +can be accessed using references `{module}` (either as `const&` or `&`). These +holders hold the actual option data for the specific module. + +The holder types are forward declared and can thus only be accessed if one also +includes the appropriate `{module}_options.h`, which contains the proper +declaration for the holder class. + + +Option modules +-------------- + +Every option module declares an "option holder" class, which is a simple struct +that has two members for every option (that is not declared as `type = void`): +the actual option value as `{option.type} {option.name}` and a Boolean flag +`bool {option.name}__setByUser` that indicates whether the option value was +explicitly set by the user. If any of the options of a module is a mode option, +the option module also defines an enum class that corresponds to the mode, +including `operator<<()` and `stringTo{mode type}`. + +For convenience, the option modules also provide methods `void +{module.id}::setDefault{option.name}(Options& opts, {option.type} value)`. Each +such method sets the option value to the given value, if the option was not yet +set by the user, i.e., the `__setByUser` flag is false. Additionally, every +option module exports the `long` option name as `static constexpr const char* +{module.id}::{option.name}__name`. + + +Full Example +============ + + [[option]] + category = "regular" + name = "decisionMode" + long = "decision=MODE" + alias = ["decision-mode"] + type = "DecisionMode" + default = "INTERNAL" + predicates = ["setDecisionModeStopOnly"] + help = "choose decision mode, see --decision=help" + help_mode = "Decision modes." + [[option.mode.INTERNAL]] + name = "internal" + help = "Use the internal decision heuristics of the SAT solver." + [[option.mode.JUSTIFICATION]] + name = "justification" + help = "An ATGP-inspired justification heuristic." + [[option.mode.RELEVANCY]] + name = "justification-stoponly" + help = "Use the justification heuristic only to stop early, not for decisions." + +This defines a new option that is accessible via +`d_options.{module.id}.decisionMode` and stores an automatically generated mode +`DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and +`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also +with `--decision-mode=justification`, and similarly from an SMT-LIB input with +`(set-option :decision internal)` and `(set-option :decision-mode +justification)`. The command-line help for this option looks as follows: + + --output-lang=LANG | --output-language=LANG + force output language (default is "auto"; see + --output-lang help) diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h deleted file mode 100644 index 86112a907..000000000 --- a/src/options/base_handlers.h +++ /dev/null @@ -1,87 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include "cvc5_private.h" - -#ifndef CVC5__BASE_HANDLERS_H -#define CVC5__BASE_HANDLERS_H - -#include <iostream> -#include <string> -#include <sstream> - -#include "options/option_exception.h" - -namespace cvc5 { -namespace options { - -template <template <class U> class Cmp> -class comparator { - long d_lbound; - double d_dbound; - bool d_hasLbound; - - public: - comparator(int i) : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {} - comparator(long l) : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} - comparator(double d) : d_lbound(0), d_dbound(d), d_hasLbound(false) {} - template <class T> - void operator()(std::string option, const T& value) { - if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) || - (!d_hasLbound && !(Cmp<T>()(value, T(d_dbound))))) { - std::stringstream ss; - ss << option << ": " << value << " is not a legal setting"; - throw OptionException(ss.str()); - } - } -};/* class comparator */ - -struct greater : public comparator<std::greater> { - greater(int i) : comparator<std::greater>(i) {} - greater(long l) : comparator<std::greater>(l) {} - greater(double d) : comparator<std::greater>(d) {} -};/* struct greater */ - -struct greater_equal : public comparator<std::greater_equal> { - greater_equal(int i) : comparator<std::greater_equal>(i) {} - greater_equal(long l) : comparator<std::greater_equal>(l) {} - greater_equal(double d) : comparator<std::greater_equal>(d) {} -};/* struct greater_equal */ - -struct less : public comparator<std::less> { - less(int i) : comparator<std::less>(i) {} - less(long l) : comparator<std::less>(l) {} - less(double d) : comparator<std::less>(d) {} -};/* struct less */ - -struct less_equal : public comparator<std::less_equal> { - less_equal(int i) : comparator<std::less_equal>(i) {} - less_equal(long l) : comparator<std::less_equal>(l) {} - less_equal(double d) : comparator<std::less_equal>(d) {} -};/* struct less_equal */ - -struct not_equal : public comparator<std::not_equal_to> { - not_equal(int i) : comparator<std::not_equal_to>(i) {} - not_equal(long l) : comparator<std::not_equal_to>(l) {} - not_equal(double d) : comparator<std::not_equal_to>(d) {} -};/* struct not_equal_to */ - -} // namespace options -} // namespace cvc5 - -#endif /* CVC5__BASE_HANDLERS_H */ diff --git a/src/options/base_options.toml b/src/options/base_options.toml index f9d1c1a18..64d373509 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -1,5 +1,6 @@ id = "BASE" name = "Base" +public = true [[option]] name = "in" @@ -76,6 +77,15 @@ name = "Base" help = "decrease verbosity (may be repeated)" [[option]] + name = "incrementalSolving" + category = "common" + short = "i" + long = "incremental" + type = "bool" + default = "true" + help = "enable incremental solving" + +[[option]] name = "statistics" long = "stats" category = "common" @@ -144,3 +154,52 @@ name = "Base" long = "print-success" type = "bool" help = "print the \"success\" output required of SMT-LIBv2" + +[[option]] + name = "cumulativeMillisecondLimit" + category = "common" + long = "tlimit=MS" + type = "uint64_t" + help = "set time limit in milliseconds of wall clock time" + +[[option]] + name = "perCallMillisecondLimit" + category = "common" + long = "tlimit-per=MS" + type = "uint64_t" + help = "set time limit per query in milliseconds" + +[[option]] + name = "cumulativeResourceLimit" + category = "common" + long = "rlimit=N" + type = "uint64_t" + help = "set resource limit" + +[[option]] + name = "perCallResourceLimit" + alias = ["reproducible-resource-limit"] + category = "common" + long = "rlimit-per=N" + type = "uint64_t" + help = "set resource limit per query" + +# --rweight is used to override the default of one particular resource weight. +# It can be given multiple times to override multiple weights. When options are +# parsed, the resource manager might now be created yet, and it is not clear +# how an option handler would access it in a reasonable way. The option handler +# thus merely puts the data in another option that holds a vector of strings. +# This other option "resourceWeightHolder" has the sole purpose of storing +# this data in a way so that the resource manager can access it in its +# constructor. +[[option]] + category = "expert" + long = "rweight=VAL=N" + type = "std::string" + handler = "setResourceWeight" + help = "set a single resource weight" + +[[option]] + name = "resourceWeightHolder" + category = "undocumented" + type = "std::vector<std::string>" diff --git a/src/options/main_options.toml b/src/options/main_options.toml index e8bb8ea72..19bb97f34 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -87,3 +87,51 @@ public = true type = "bool" default = "false" help = "spin on segfault/other crash waiting for gdb" + +[[option]] + name = "dumpModels" + category = "regular" + long = "dump-models" + type = "bool" + default = "false" + help = "output models after every SAT/INVALID/UNKNOWN response" + +[[option]] + name = "dumpProofs" + category = "regular" + long = "dump-proofs" + type = "bool" + default = "false" + help = "output proofs after every UNSAT/VALID response" + +[[option]] + name = "dumpInstantiations" + category = "regular" + long = "dump-instantiations" + type = "bool" + default = "false" + help = "output instantiations of quantified formulas after every UNSAT/VALID response" + +[[option]] + name = "dumpUnsatCores" + category = "regular" + long = "dump-unsat-cores" + type = "bool" + default = "false" + help = "output unsat cores after every UNSAT/VALID response" + +[[option]] + name = "dumpUnsatCoresFull" + category = "regular" + long = "dump-unsat-cores-full" + type = "bool" + default = "false" + help = "dump the full unsat core, including unlabeled assertions" + +[[option]] + name = "forceNoLimitCpuWhileDump" + category = "regular" + long = "force-no-limit-cpu-while-dump" + type = "bool" + default = "false" + help = "Force no CPU limit when dumping models and proofs"
\ No newline at end of file diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 7e1cf68e4..e2fbd4cf1 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -210,6 +210,30 @@ def get_holder_ref_decls(modules): return concat_format(' options::Holder{id_cap}& {id};', modules) +def get_handler(option): + """Render handler call for assignment functions""" + optname = option.long_name if option.long else "" + if option.handler: + if option.type == 'void': + return 'opts.handler().{}("{}", option)'.format(option.handler, optname) + else: + return 'opts.handler().{}("{}", option, optionarg)'.format(option.handler, optname) + elif option.mode: + return 'stringTo{}(optionarg)'.format(option.type) + elif option.type != 'bool': + return 'handleOption<{}>("{}", option, optionarg)'.format(option.type, optname) + return None + + +def get_predicates(option): + """Render predicate calls for assignment functions""" + if not option.predicates: + return [] + optname = option.long_name if option.long else "" + assert option.type != 'void' + return ['opts.handler().{}("{}", option, value);'.format(x, optname) + for x in option.predicates] + class Module(object): """Options module. @@ -713,31 +737,10 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ sphinxgen.add(module, option) # Generate handler call - handler = None - if option.handler: - if option.type == 'void': - handler = 'opts.handler().{}(option)'.format(option.handler) - else: - handler = \ - 'opts.handler().{}(option, optionarg)'.format(option.handler) - elif option.mode: - handler = 'stringTo{}(optionarg)'.format(option.type) - elif option.type != 'bool': - handler = \ - 'handleOption<{}>(option, optionarg)'.format(option.type) + handler = get_handler(option) # Generate predicate calls - predicates = [] - if option.predicates: - if option.type == 'bool': - predicates = \ - ['opts.handler().{}(option, value);'.format(x) \ - for x in option.predicates] - else: - assert option.type != 'void' - predicates = \ - ['opts.handler().{}(option, value);'.format(x) \ - for x in option.predicates] + predicates = get_predicates(option) # Generate options_handler and getopt_long cases = [] @@ -813,7 +816,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ name=option.name, option='key')) elif option.handler: - h = 'handler->{handler}("{smtname}"' + h = 'handler->{handler}("{smtname}", key' if argument_req: h += ', optionarg' h += ');' diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index c1c843802..07138dce3 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -33,7 +33,6 @@ #include "options/didyoumean.h" #include "options/language.h" #include "options/option_exception.h" -#include "options/resource_manager_options.h" #include "options/smt_options.h" #include "options/theory_options.h" @@ -68,10 +67,11 @@ void throwLazyBBUnsupported(options::SatSolverMode m) OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } -unsigned long OptionsHandler::limitHandler(std::string option, - std::string optarg) +uint64_t OptionsHandler::limitHandler(const std::string& option, + const std::string& flag, + const std::string& optarg) { - unsigned long ms; + uint64_t ms; std::istringstream convert(optarg); if (!(convert >> ms)) { @@ -81,14 +81,18 @@ unsigned long OptionsHandler::limitHandler(std::string option, return ms; } -void OptionsHandler::setResourceWeight(std::string option, std::string optarg) +void OptionsHandler::setResourceWeight(const std::string& option, + const std::string& flag, + const std::string& optarg) { - d_options->resman.resourceWeightHolder.emplace_back(optarg); + d_options->base.resourceWeightHolder.emplace_back(optarg); } // theory/quantifiers/options_handlers.h -void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) +void OptionsHandler::checkInstWhenMode(const std::string& option, + const std::string& flag, + InstWhenMode mode) { if (mode == InstWhenMode::PRE_FULL) { @@ -98,7 +102,9 @@ void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) } // theory/bv/options_handlers.h -void OptionsHandler::abcEnabledBuild(std::string option, bool value) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + bool value) { #ifndef CVC5_USE_ABC if(value) { @@ -111,7 +117,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, bool value) #endif /* CVC5_USE_ABC */ } -void OptionsHandler::abcEnabledBuild(std::string option, std::string value) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + const std::string& value) { #ifndef CVC5_USE_ABC if(!value.empty()) { @@ -124,7 +132,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) #endif /* CVC5_USE_ABC */ } -void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) +void OptionsHandler::checkBvSatSolver(const std::string& option, + const std::string& flag, + SatSolverMode m) { if (m == SatSolverMode::CRYPTOMINISAT && !Configuration::isBuiltWithCryptominisat()) @@ -136,15 +146,6 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) throw OptionException(ss.str()); } - if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical()) - { - std::stringstream ss; - ss << "option `" << option - << "' requires a CaDiCaL build of cvc5; this binary was not built with " - "CaDiCaL support"; - throw OptionException(ss.str()); - } - if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat()) { std::stringstream ss; @@ -167,7 +168,9 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) } } -void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) +void OptionsHandler::checkBitblastMode(const std::string& option, + const std::string& flag, + BitblastMode m) { if (m == options::BitblastMode::LAZY) { @@ -186,7 +189,9 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) } } -void OptionsHandler::setBitblastAig(std::string option, bool arg) +void OptionsHandler::setBitblastAig(const std::string& option, + const std::string& flag, + bool arg) { if(arg) { if (d_options->bv.bitblastModeWasSetByUser) { @@ -212,8 +217,9 @@ szs\n\ + Print instantiations as SZS compliant proof.\n\ "; -InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, - std::string optarg) +InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "default") { return InstFormatMode::DEFAULT; @@ -229,24 +235,30 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, } // decision/options_handlers.h -void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m) +void OptionsHandler::setDecisionModeStopOnly(const std::string& option, + const std::string& flag, + DecisionMode m) { d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY); } -void OptionsHandler::setProduceAssertions(std::string option, bool value) +void OptionsHandler::setProduceAssertions(const std::string& option, + const std::string& flag, + bool value) { d_options->smt.produceAssertions = value; d_options->smt.interactiveMode = value; } -void OptionsHandler::setStats(const std::string& option, bool value) +void OptionsHandler::setStats(const std::string& option, + const std::string& flag, + bool value) { #ifndef CVC5_STATISTICS_ON if (value) { std::stringstream ss; - ss << "option `" << option + ss << "option `" << flag << "' requires a statistics-enabled build of cvc5; this binary was not " "built with statistics support"; throw OptionException(ss.str()); @@ -283,18 +295,25 @@ void OptionsHandler::setStats(const std::string& option, bool value) } } -void OptionsHandler::threadN(std::string option) { - throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); +void OptionsHandler::threadN(const std::string& option, const std::string& flag) +{ + throw OptionException(flag + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); } // expr/options_handlers.h -void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) { +void OptionsHandler::setDefaultExprDepthPredicate(const std::string& option, + const std::string& flag, + int depth) +{ if(depth < -1) { throw OptionException("--expr-depth requires a positive argument, or -1."); } } -void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) { +void OptionsHandler::setDefaultDagThreshPredicate(const std::string& option, + const std::string& flag, + int dag) +{ if(dag < 0) { throw OptionException("--dag-thresh requires a nonnegative argument."); } @@ -313,12 +332,16 @@ static void print_config_cond (const char * str, bool cond = false) { print_config(str, cond ? "yes" : "no"); } -void OptionsHandler::copyright(std::string option) { +void OptionsHandler::copyright(const std::string& option, + const std::string& flag) +{ std::cout << Configuration::copyright() << std::endl; exit(0); } -void OptionsHandler::showConfiguration(std::string option) { +void OptionsHandler::showConfiguration(const std::string& option, + const std::string& flag) +{ std::cout << Configuration::about() << std::endl; print_config ("version", Configuration::getVersionString()); @@ -365,13 +388,11 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("abc", Configuration::isBuiltWithAbc()); print_config_cond("cln", Configuration::isBuiltWithCln()); print_config_cond("glpk", Configuration::isBuiltWithGlpk()); - print_config_cond("cadical", Configuration::isBuiltWithCadical()); print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); print_config_cond("kissat", Configuration::isBuiltWithKissat()); print_config_cond("poly", Configuration::isBuiltWithPoly()); print_config_cond("editline", Configuration::isBuiltWithEditline()); - print_config_cond("symfpu", Configuration::isBuiltWithSymFPU()); exit(0); } @@ -386,7 +407,8 @@ static void printTags(unsigned ntags, char const* const* tags) std::cout << std::endl; } -void OptionsHandler::showDebugTags(std::string option) +void OptionsHandler::showDebugTags(const std::string& option, + const std::string& flag) { if (!Configuration::isDebugBuild()) { @@ -400,7 +422,8 @@ void OptionsHandler::showDebugTags(std::string option) exit(0); } -void OptionsHandler::showTraceTags(std::string option) +void OptionsHandler::showTraceTags(const std::string& option, + const std::string& flag) { if (!Configuration::isTracingBuild()) { @@ -432,7 +455,9 @@ static std::string suggestTags(char const* const* validTags, return didYouMean.getMatchAsString(inputTag); } -void OptionsHandler::enableTraceTag(std::string option, std::string optarg) +void OptionsHandler::enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(!Configuration::isTracingBuild()) { @@ -454,7 +479,9 @@ void OptionsHandler::enableTraceTag(std::string option, std::string optarg) Trace.on(optarg); } -void OptionsHandler::enableDebugTag(std::string option, std::string optarg) +void OptionsHandler::enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { if (!Configuration::isDebugBuild()) { @@ -485,8 +512,9 @@ void OptionsHandler::enableDebugTag(std::string option, std::string optarg) Trace.on(optarg); } -OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, - std::string optarg) +OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; @@ -503,8 +531,9 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, Unreachable(); } -InputLanguage OptionsHandler::stringToInputLanguage(std::string option, - std::string optarg) +InputLanguage OptionsHandler::stringToInputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; @@ -521,7 +550,9 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option, } /* options/base_options_handlers.h */ -void OptionsHandler::setVerbosity(std::string option, int value) +void OptionsHandler::setVerbosity(const std::string& option, + const std::string& flag, + int value) { if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&cvc5::null_os); @@ -551,14 +582,18 @@ void OptionsHandler::setVerbosity(std::string option, int value) } } -void OptionsHandler::increaseVerbosity(std::string option) { +void OptionsHandler::increaseVerbosity(const std::string& option, + const std::string& flag) +{ d_options->base.verbosity += 1; - setVerbosity(option, options::verbosity()); + setVerbosity(option, flag, d_options->base.verbosity); } -void OptionsHandler::decreaseVerbosity(std::string option) { +void OptionsHandler::decreaseVerbosity(const std::string& option, + const std::string& flag) +{ d_options->base.verbosity -= 1; - setVerbosity(option, options::verbosity()); + setVerbosity(option, flag, d_options->base.verbosity); } } // namespace options diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 4b9b1c0ae..3b3f80e6c 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -19,9 +19,9 @@ #define CVC5__OPTIONS__OPTIONS_HANDLER_H #include <ostream> +#include <sstream> #include <string> -#include "options/base_handlers.h" #include "options/bv_options.h" #include "options/decision_options.h" #include "options/language.h" @@ -44,72 +44,117 @@ class OptionsHandler { public: OptionsHandler(Options* options); - void unsignedGreater0(const std::string& option, unsigned value) { - options::greater(0)(option, value); + template <typename T> + void geqZero(const std::string& option, + const std::string& flag, + T value) const + { + if (value < 0) + { + std::stringstream ss; + ss << flag << ": " << value << " is not a legal setting, should be " + << value << " >= 0."; + throw OptionException(ss.str()); + } } - - void unsignedLessEqual2(const std::string& option, unsigned value) { - options::less_equal(2)(option, value); - } - - void doubleGreaterOrEqual0(const std::string& option, double value) { - options::greater_equal(0.0)(option, value); - } - - void doubleLessOrEqual1(const std::string& option, double value) { - options::less_equal(1.0)(option, value); + template <typename T> + void betweenZeroAndOne(const std::string& option, + const std::string& flag, + T value) const + { + if (value < 0 || value > 1) + { + std::stringstream ss; + ss << flag << ": " << value + << " is not a legal setting, should be 0 <= " << flag << " <= 1."; + throw OptionException(ss.str()); + } } // theory/quantifiers/options_handlers.h - void checkInstWhenMode(std::string option, InstWhenMode mode); + void checkInstWhenMode(const std::string& option, + const std::string& flag, + InstWhenMode mode); // theory/bv/options_handlers.h - void abcEnabledBuild(std::string option, bool value); - void abcEnabledBuild(std::string option, std::string value); - - template<class T> void checkSatSolverEnabled(std::string option, T m); - - void checkBvSatSolver(std::string option, SatSolverMode m); - void checkBitblastMode(std::string option, BitblastMode m); - - void setBitblastAig(std::string option, bool arg); + void abcEnabledBuild(const std::string& option, + const std::string& flag, + bool value); + void abcEnabledBuild(const std::string& option, + const std::string& flag, + const std::string& value); + + void checkBvSatSolver(const std::string& option, + const std::string& flag, + SatSolverMode m); + void checkBitblastMode(const std::string& option, + const std::string& flag, + BitblastMode m); + + void setBitblastAig(const std::string& option, + const std::string& flag, + bool arg); // printer/options_handlers.h - InstFormatMode stringToInstFormatMode(std::string option, std::string optarg); + InstFormatMode stringToInstFormatMode(const std::string& option, + const std::string& flag, + const std::string& optarg); // decision/options_handlers.h - void setDecisionModeStopOnly(std::string option, DecisionMode m); + void setDecisionModeStopOnly(const std::string& option, + const std::string& flag, + DecisionMode m); /** * Throws a ModalException if this option is being set after final * initialization. */ - void setProduceAssertions(std::string option, bool value); + void setProduceAssertions(const std::string& option, + const std::string& flag, + bool value); - void setStats(const std::string& option, bool value); + void setStats(const std::string& option, const std::string& flag, bool value); - unsigned long limitHandler(std::string option, std::string optarg); - void setResourceWeight(std::string option, std::string optarg); + uint64_t limitHandler(const std::string& option, + const std::string& flag, + const std::string& optarg); + void setResourceWeight(const std::string& option, + const std::string& flag, + const std::string& optarg); /* expr/options_handlers.h */ - void setDefaultExprDepthPredicate(std::string option, int depth); - void setDefaultDagThreshPredicate(std::string option, int dag); + void setDefaultExprDepthPredicate(const std::string& option, + const std::string& flag, + int depth); + void setDefaultDagThreshPredicate(const std::string& option, + const std::string& flag, + int dag); /* main/options_handlers.h */ - void copyright(std::string option); - void showConfiguration(std::string option); - void showDebugTags(std::string option); - void showTraceTags(std::string option); - void threadN(std::string option); + void copyright(const std::string& option, const std::string& flag); + void showConfiguration(const std::string& option, const std::string& flag); + void showDebugTags(const std::string& option, const std::string& flag); + void showTraceTags(const std::string& option, const std::string& flag); + void threadN(const std::string& option, const std::string& flag); /* options/base_options_handlers.h */ - void setVerbosity(std::string option, int value); - void increaseVerbosity(std::string option); - void decreaseVerbosity(std::string option); - OutputLanguage stringToOutputLanguage(std::string option, std::string optarg); - InputLanguage stringToInputLanguage(std::string option, std::string optarg); - void enableTraceTag(std::string option, std::string optarg); - void enableDebugTag(std::string option, std::string optarg); + void setVerbosity(const std::string& option, + const std::string& flag, + int value); + void increaseVerbosity(const std::string& option, const std::string& flag); + void decreaseVerbosity(const std::string& option, const std::string& flag); + OutputLanguage stringToOutputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg); + InputLanguage stringToInputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg); + void enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg); + void enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg); private: @@ -121,18 +166,6 @@ public: }; /* class OptionHandler */ -template<class T> -void OptionsHandler::checkSatSolverEnabled(std::string option, T m) -{ -#if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \ - && !defined(CVC5_USE_KISSAT) - std::stringstream ss; - ss << "option `" << option - << "' requires cvc5 to be built with CryptoMiniSat or CaDiCaL or Kissat"; - throw OptionException(ss.str()); -#endif -} - } // namespace options } // namespace cvc5 diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp index 35e891f5a..552058312 100644 --- a/src/options/options_public.cpp +++ b/src/options/options_public.cpp @@ -17,118 +17,10 @@ #include "options_public.h" -#include <fstream> -#include <ostream> -#include <string> -#include <vector> - -#include "base/listener.h" -#include "base/modal_exception.h" -#include "options/base_options.h" -#include "options/language.h" -#include "options/main_options.h" -#include "options/option_exception.h" -#include "options/options.h" -#include "options/parser_options.h" -#include "options/printer_modes.h" -#include "options/printer_options.h" -#include "options/resource_manager_options.h" -#include "options/smt_options.h" #include "options/uf_options.h" namespace cvc5::options { -InputLanguage getInputLanguage(const Options& opts) -{ - return opts.base.inputLanguage; -} -InstFormatMode getInstFormatMode(const Options& opts) -{ - return opts.printer.instFormatMode; -} -OutputLanguage getOutputLanguage(const Options& opts) -{ - return opts.base.outputLanguage; -} bool getUfHo(const Options& opts) { return opts.uf.ufHo; } -bool getDumpInstantiations(const Options& opts) -{ - return opts.smt.dumpInstantiations; -} -bool getDumpModels(const Options& opts) { return opts.smt.dumpModels; } -bool getDumpProofs(const Options& opts) { return opts.smt.dumpProofs; } -bool getDumpUnsatCores(const Options& opts) -{ - return opts.smt.dumpUnsatCores || opts.smt.dumpUnsatCoresFull; -} -bool getFilesystemAccess(const Options& opts) -{ - return opts.parser.filesystemAccess; -} -bool getForceNoLimitCpuWhileDump(const Options& opts) -{ - return opts.smt.forceNoLimitCpuWhileDump; -} -bool getIncrementalSolving(const Options& opts) -{ - return opts.smt.incrementalSolving; -} -bool getLanguageHelp(const Options& opts) { return opts.base.languageHelp; } -bool getMemoryMap(const Options& opts) { return opts.parser.memoryMap; } -bool getParseOnly(const Options& opts) { return opts.base.parseOnly; } -bool getProduceModels(const Options& opts) { return opts.smt.produceModels; } -bool getSemanticChecks(const Options& opts) -{ - return opts.parser.semanticChecks; -} -bool getStatistics(const Options& opts) { return opts.base.statistics; } -bool getStatsEveryQuery(const Options& opts) -{ - return opts.base.statisticsEveryQuery; -} -bool getStrictParsing(const Options& opts) -{ - return opts.parser.strictParsing; -} -uint64_t getCumulativeTimeLimit(const Options& opts) -{ - return opts.resman.cumulativeMillisecondLimit; -} -const std::string& getForceLogicString(const Options& opts) -{ - return opts.parser.forceLogicString; -} -int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; } - -std::istream* getIn(const Options& opts) { return opts.base.in; } -std::ostream* getErr(const Options& opts) { return opts.base.err; } -std::ostream* getOut(const Options& opts) { return opts.base.out; } - -void setInputLanguage(InputLanguage val, Options& opts) -{ - opts.base.inputLanguage = val; -} -void setOut(std::ostream* val, Options& opts) { opts.base.out = val; } -void setOutputLanguage(OutputLanguage val, Options& opts) -{ - opts.base.outputLanguage = val; -} - -bool wasSetByUserEarlyExit(const Options& opts) -{ - return opts.driver.earlyExitWasSetByUser; -} -bool wasSetByUserForceLogicString(const Options& opts) -{ - return opts.parser.forceLogicStringWasSetByUser; -} -bool wasSetByUserIncrementalSolving(const Options& opts) -{ - return opts.smt.incrementalSolvingWasSetByUser; -} -bool wasSetByUserInteractive(const Options& opts) -{ - return opts.driver.interactiveWasSetByUser; -} } // namespace cvc5::options diff --git a/src/options/options_public.h b/src/options/options_public.h index 1d2f9edba..60929c96c 100644 --- a/src/options/options_public.h +++ b/src/options/options_public.h @@ -23,47 +23,11 @@ #ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H #define CVC5__OPTIONS__OPTIONS_PUBLIC_H -#include "options/language.h" #include "options/options.h" -#include "options/printer_modes.h" namespace cvc5::options { -InputLanguage getInputLanguage(const Options& opts) CVC5_EXPORT; -InstFormatMode getInstFormatMode(const Options& opts) CVC5_EXPORT; -OutputLanguage getOutputLanguage(const Options& opts) CVC5_EXPORT; bool getUfHo(const Options& opts) CVC5_EXPORT; -bool getDumpInstantiations(const Options& opts) CVC5_EXPORT; -bool getDumpModels(const Options& opts) CVC5_EXPORT; -bool getDumpProofs(const Options& opts) CVC5_EXPORT; -bool getDumpUnsatCores(const Options& opts) CVC5_EXPORT; -bool getFilesystemAccess(const Options& opts) CVC5_EXPORT; -bool getForceNoLimitCpuWhileDump(const Options& opts) CVC5_EXPORT; -bool getIncrementalSolving(const Options& opts) CVC5_EXPORT; -bool getLanguageHelp(const Options& opts) CVC5_EXPORT; -bool getMemoryMap(const Options& opts) CVC5_EXPORT; -bool getParseOnly(const Options& opts) CVC5_EXPORT; -bool getProduceModels(const Options& opts) CVC5_EXPORT; -bool getSemanticChecks(const Options& opts) CVC5_EXPORT; -bool getStatistics(const Options& opts) CVC5_EXPORT; -bool getStatsEveryQuery(const Options& opts) CVC5_EXPORT; -bool getStrictParsing(const Options& opts) CVC5_EXPORT; -uint64_t getCumulativeTimeLimit(const Options& opts) CVC5_EXPORT; -const std::string& getForceLogicString(const Options& opts) CVC5_EXPORT; -int32_t getVerbosity(const Options& opts) CVC5_EXPORT; - -std::istream* getIn(const Options& opts) CVC5_EXPORT; -std::ostream* getErr(const Options& opts) CVC5_EXPORT; -std::ostream* getOut(const Options& opts) CVC5_EXPORT; - -void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT; -void setOut(std::ostream* val, Options& opts) CVC5_EXPORT; -void setOutputLanguage(OutputLanguage val, Options& opts) CVC5_EXPORT; - -bool wasSetByUserEarlyExit(const Options& opts) CVC5_EXPORT; -bool wasSetByUserForceLogicString(const Options& opts) CVC5_EXPORT; -bool wasSetByUserIncrementalSolving(const Options& opts) CVC5_EXPORT; -bool wasSetByUserInteractive(const Options& opts) CVC5_EXPORT; } // namespace cvc5::options diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index e909a5f0a..2c22065c2 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -58,7 +58,6 @@ extern int optreset; ${headers_module}$ #include "base/cvc5config.h" -#include "options/base_handlers.h" ${headers_handler}$ @@ -82,7 +81,9 @@ thread_local Options* Options::s_current = NULL; */ template <class T, bool is_numeric, bool is_integer> struct OptionHandler { - static T handle(std::string option, std::string optionarg); + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg); };/* struct OptionHandler<> */ /** Variant for integral C++ types */ @@ -99,32 +100,35 @@ struct OptionHandler<T, true, true> { return str.find('-') != std::string::npos; } - static T handle(const std::string& option, const std::string& optionarg) { + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { try { T i; bool success = stringToInt(i, optionarg); if(!success){ - throw OptionException(option + ": failed to parse "+ optionarg + - " as an integer of the appropriate type."); + throw OptionException(flag + ": failed to parse " + optionarg + + " as an integer of the appropriate type."); } // Depending in the platform unsigned numbers with '-' signs may parse. // Reject these by looking for any minus if it is not signed. if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) { // unsigned type but user gave negative argument - throw OptionException(option + " requires a nonnegative argument"); + throw OptionException(flag + " requires a nonnegative argument"); } else if(i < std::numeric_limits<T>::min()) { // negative overflow for type std::stringstream ss; - ss << option << " requires an argument >= " - << std::numeric_limits<T>::min(); + ss << flag + << " requires an argument >= " << std::numeric_limits<T>::min(); throw OptionException(ss.str()); } else if(i > std::numeric_limits<T>::max()) { // positive overflow for type std::stringstream ss; - ss << option << " requires an argument <= " - << std::numeric_limits<T>::max(); + ss << flag + << " requires an argument <= " << std::numeric_limits<T>::max(); throw OptionException(ss.str()); } @@ -137,7 +141,7 @@ struct OptionHandler<T, true, true> { // } } catch(std::invalid_argument&) { // user gave something other than an integer - throw OptionException(option + " requires an integer argument"); + throw OptionException(flag + " requires an integer argument"); } } };/* struct OptionHandler<T, true, true> */ @@ -145,29 +149,33 @@ struct OptionHandler<T, true, true> { /** Variant for numeric but non-integral C++ types */ template <class T> struct OptionHandler<T, true, false> { - static T handle(std::string option, std::string optionarg) { - std::stringstream in(optionarg); + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { + std::stringstream inss(optionarg); long double r; - in >> r; - if(! in.eof()) { + inss >> r; + if (!inss.eof()) + { // we didn't consume the whole string (junk at end) - throw OptionException(option + " requires a numeric argument"); + throw OptionException(flag + " requires a numeric argument"); } if(! std::numeric_limits<T>::is_signed && r < 0.0) { // unsigned type but user gave negative value - throw OptionException(option + " requires a nonnegative argument"); + throw OptionException(flag + " requires a nonnegative argument"); } else if(r < -std::numeric_limits<T>::max()) { // negative overflow for type std::stringstream ss; - ss << option << " requires an argument >= " - << -std::numeric_limits<T>::max(); + ss << flag + << " requires an argument >= " << -std::numeric_limits<T>::max(); throw OptionException(ss.str()); } else if(r > std::numeric_limits<T>::max()) { // positive overflow for type std::stringstream ss; - ss << option << " requires an argument <= " - << std::numeric_limits<T>::max(); + ss << flag + << " requires an argument <= " << std::numeric_limits<T>::max(); throw OptionException(ss.str()); } @@ -178,7 +186,10 @@ struct OptionHandler<T, true, false> { /** Variant for non-numeric C++ types */ template <class T> struct OptionHandler<T, false, false> { - static T handle(std::string option, std::string optionarg) { + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { T::unsupported_handleOption_call___please_write_me; // The above line causes a compiler error if this version of the template // is ever instantiated (meaning that a specialization is missing). So @@ -191,36 +202,26 @@ struct OptionHandler<T, false, false> { /** Handle an option of type T in the default way. */ template <class T> -T handleOption(std::string option, std::string optionarg) { - return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg); +T handleOption(const std::string& option, + const std::string& flag, + const std::string& optionarg) +{ + return OptionHandler<T, + std::numeric_limits<T>::is_specialized, + std::numeric_limits<T>::is_integer>::handle(option, + flag, + optionarg); } /** Handle an option of type std::string in the default way. */ template <> -std::string handleOption<std::string>(std::string option, std::string optionarg) { +std::string handleOption<std::string>(const std::string& option, + const std::string& flag, + const std::string& optionarg) +{ return optionarg; } -/** - * Run handler, and any user-given predicates, for option T. - * If a user specifies a :handler or :predicates, it overrides this. - */ -template <class T> -typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, options::OptionsHandler* handler) { - // By default, parse the option argument in a way appropriate for its type. - // E.g., for "unsigned int" options, ensure that the provided argument is - // a nonnegative integer that fits in the unsigned int type. - - return handleOption<typename T::type>(option, optionarg); -} - -template <class T> -void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* handler) { - // By default, nothing to do for bool. Users add things with - // :predicate in options files to provide custom checking routines - // that can throw exceptions. -} - Options::Options(OptionsListener* ol) : d_handler(new options::OptionsHandler(this)), // clang-format off diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 6fc683368..f19b903a6 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -1,5 +1,6 @@ id = "PARSER" name = "Parser" +public = true [[option]] name = "strictParsing" diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml index 26d7a451b..eda5ea963 100644 --- a/src/options/prop_options.toml +++ b/src/options/prop_options.toml @@ -8,7 +8,7 @@ name = "SAT Layer" long = "random-freq=P" type = "double" default = "0.0" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "sets the frequency of random decisions in the sat solver (P=0.0 by default)" [[option]] @@ -24,7 +24,7 @@ name = "SAT Layer" category = "regular" type = "double" default = "0.95" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "variable activity decay factor for Minisat" [[option]] @@ -32,7 +32,7 @@ name = "SAT Layer" category = "regular" type = "double" default = "0.999" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "clause activity decay factor for Minisat" [[option]] @@ -49,7 +49,7 @@ name = "SAT Layer" long = "restart-int-inc=F" type = "double" default = "3.0" - predicates = ["doubleGreaterOrEqual0"] + predicates = ["geqZero"] help = "sets the restart interval increase factor for the sat solver (F=3.0 by default)" [[option]] diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml deleted file mode 100644 index 6d5c4d4cf..000000000 --- a/src/options/resource_manager_options.toml +++ /dev/null @@ -1,51 +0,0 @@ -id = "RESMAN" -name = "Resource Manager" - -[[option]] - name = "cumulativeMillisecondLimit" - category = "common" - long = "tlimit=MS" - type = "uint64_t" - help = "set time limit in milliseconds of wall clock time" - -[[option]] - name = "perCallMillisecondLimit" - category = "common" - long = "tlimit-per=MS" - type = "uint64_t" - help = "set time limit per query in milliseconds" - -[[option]] - name = "cumulativeResourceLimit" - category = "common" - long = "rlimit=N" - type = "uint64_t" - help = "set resource limit" - -[[option]] - name = "perCallResourceLimit" - alias = ["reproducible-resource-limit"] - category = "common" - long = "rlimit-per=N" - type = "uint64_t" - help = "set resource limit per query" - -# --rweight is used to override the default of one particular resource weight. -# It can be given multiple times to override multiple weights. When options are -# parsed, the resource manager might now be created yet, and it is not clear -# how an option handler would access it in a reasonable way. The option handler -# thus merely puts the data in another option that holds a vector of strings. -# This other option "resourceWeightHolder" has the sole purpose of storing -# this data in a way so that the resource manager can access it in its -# constructor. -[[option]] - category = "expert" - long = "rweight=VAL=N" - type = "std::string" - handler = "setResourceWeight" - help = "set a single resource weight" - -[[option]] - name = "resourceWeightHolder" - category = "undocumented" - type = "std::vector<std::string>" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index d1354f777..4d08aa672 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -79,14 +79,6 @@ name = "SMT Layer" help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions" [[option]] - name = "dumpModels" - category = "regular" - long = "dump-models" - type = "bool" - default = "false" - help = "output models after every SAT/INVALID/UNKNOWN response" - -[[option]] name = "modelCoresMode" category = "regular" long = "model-cores=MODE" @@ -131,14 +123,6 @@ name = "SMT Layer" help = "produce proofs, support check-proofs and get-proof" [[option]] - name = "dumpProofs" - category = "regular" - long = "dump-proofs" - type = "bool" - default = "false" - help = "output proofs after every UNSAT/VALID response" - -[[option]] name = "checkProofs" category = "regular" long = "check-proofs" @@ -146,14 +130,6 @@ name = "SMT Layer" help = "after UNSAT/VALID, check the generated proof (with proof)" [[option]] - name = "dumpInstantiations" - category = "regular" - long = "dump-instantiations" - type = "bool" - default = "false" - help = "output instantiations of quantified formulas after every UNSAT/VALID response" - -[[option]] name = "sygusOut" category = "regular" long = "sygus-out=MODE" @@ -218,22 +194,6 @@ name = "SMT Layer" help = "after UNSAT/VALID, produce and check an unsat core (expensive)" [[option]] - name = "dumpUnsatCores" - category = "regular" - long = "dump-unsat-cores" - type = "bool" - default = "false" - help = "output unsat cores after every UNSAT/VALID response" - -[[option]] - name = "dumpUnsatCoresFull" - category = "regular" - long = "dump-unsat-cores-full" - type = "bool" - default = "false" - help = "dump the full unsat core, including unlabeled assertions" - -[[option]] name = "unsatAssumptions" category = "regular" long = "produce-unsat-assumptions" @@ -360,15 +320,6 @@ name = "SMT Layer" help = "calculate sort inference of input problem, convert the input based on monotonic sorts" [[option]] - name = "incrementalSolving" - category = "common" - short = "i" - long = "incremental" - type = "bool" - default = "true" - help = "enable incremental solving" - -[[option]] name = "abstractValues" category = "regular" long = "abstract-values" @@ -422,14 +373,6 @@ name = "SMT Layer" help = "set the diagnostic output channel of the solver" [[option]] - name = "forceNoLimitCpuWhileDump" - category = "regular" - long = "force-no-limit-cpu-while-dump" - type = "bool" - default = "false" - help = "Force no CPU limit when dumping models and proofs" - -[[option]] name = "foreignTheoryRewrite" category = "regular" long = "foreign-theory-rewrite" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index d96e94d43..eab982013 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -26,8 +26,8 @@ #include "base/check.h" #include "base/output.h" #include "expr/kind.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/options_public.h" #include "parser/input.h" #include "parser/parser_exception.h" #include "smt/command.h" @@ -900,7 +900,7 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s) api::Term Parser::mkStringConstant(const std::string& s) { if (language::isInputLang_smt2_6( - options::getInputLanguage(d_solver->getOptions()))) + d_solver->getOptions().base.inputLanguage)) { return d_solver->mkString(s, true); } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 1f25e00dd..816803ccc 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -21,8 +21,9 @@ #include "api/cpp/cvc5.h" #include "base/check.h" #include "cvc/cvc.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/options_public.h" +#include "options/parser_options.h" #include "parser/antlr_input.h" #include "parser/input.h" #include "parser/parser.h" @@ -120,14 +121,14 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { ParserBuilder& ParserBuilder::withOptions(const Options& opts) { ParserBuilder& retval = *this; - retval = retval.withInputLanguage(options::getInputLanguage(opts)) - .withChecks(options::getSemanticChecks(opts)) - .withStrictMode(options::getStrictParsing(opts)) - .withParseOnly(options::getParseOnly(opts)) - .withIncludeFile(options::getFilesystemAccess(opts)); - if (options::wasSetByUserForceLogicString(opts)) + retval = retval.withInputLanguage(opts.base.inputLanguage) + .withChecks(opts.parser.semanticChecks) + .withStrictMode(opts.parser.strictParsing) + .withParseOnly(opts.base.parseOnly) + .withIncludeFile(opts.parser.filesystemAccess); + if (opts.parser.forceLogicStringWasSetByUser) { - LogicInfo tmp(options::getForceLogicString(opts)); + LogicInfo tmp(opts.parser.forceLogicString); retval = retval.withForcedLogic(tmp.getLogicString()); } return retval; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 56aebdcf7..282b72974 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -17,6 +17,7 @@ #include <algorithm> #include "base/check.h" +#include "options/base_options.h" #include "options/options.h" #include "options/options_public.h" #include "parser/antlr_input.h" @@ -846,7 +847,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name) InputLanguage Smt2::getLanguage() const { - return options::getInputLanguage(d_solver->getOptions()); + return d_solver->getOptions().base.inputLanguage; } void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 89029b5eb..eb6410291 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -29,8 +29,8 @@ #include "base/check.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 15a16888d..df9d44e39 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -26,6 +26,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 5bfb2a79f..d1dd389ae 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -17,6 +17,7 @@ #include <vector> +#include "options/base_options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 79fcc4028..a5720e758 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -22,7 +22,7 @@ #include "expr/node_self_iterator.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" -#include "options/smt_options.h" +#include "options/base_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index a42b30773..c1cf0338a 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -688,9 +688,9 @@ enum class PfRule : uint32_t //================================================= Array rules // ======== Read over write // Children: (P:(not (= i1 i2))) - // Arguments: ((select (store a i2 e) i1)) + // Arguments: ((select (store a i1 e) i2)) // ---------------------------------------- - // Conclusion: (= (select (store a i2 e) i1) (select a i1)) + // Conclusion: (= (select (store a i1 e) i2) (select a i2)) ARRAYS_READ_OVER_WRITE, // ======== Read over write, contrapositive // Children: (P:(not (= (select (store a i2 e) i1) (select a i1))) diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index ec8919b0b..ddf20f5a1 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -17,8 +17,6 @@ #include "prop/cadical.h" -#ifdef CVC5_USE_CADICAL - #include "base/check.h" #include "util/statistics_registry.h" @@ -191,5 +189,3 @@ CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry, } // namespace prop } // namespace cvc5 - -#endif // CVC5_USE_CADICAL diff --git a/src/prop/cadical.h b/src/prop/cadical.h index b5e26df9f..46c7c7e42 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -20,8 +20,6 @@ #ifndef CVC5__PROP__CADICAL_H #define CVC5__PROP__CADICAL_H -#ifdef CVC5_USE_CADICAL - #include "prop/sat_solver.h" #include <cadical.hpp> @@ -103,5 +101,4 @@ class CadicalSolver : public SatSolver } // namespace prop } // namespace cvc5 -#endif // CVC5_USE_CADICAL #endif // CVC5__PROP__CADICAL_H diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f8a34ec42..4897f8e6a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -21,14 +21,15 @@ #include "base/output.h" #include "expr/node.h" #include "options/bv_options.h" +#include "printer/printer.h" #include "proof/clause_id.h" #include "prop/minisat/minisat.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" #include "smt/dump.h" #include "smt/smt_engine.h" -#include "printer/printer.h" #include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" #include "theory/theory.h" #include "theory/theory_engine.h" @@ -52,7 +53,8 @@ CnfStream::CnfStream(SatSolver* satSolver, d_registrar(registrar), d_name(name), d_removable(false), - d_resourceManager(rm) + d_resourceManager(rm), + d_stats(name) { } @@ -139,6 +141,7 @@ void CnfStream::ensureLiteral(TNode n) n.toString().c_str(), n.getType().toString().c_str()); Trace("cnf") << "ensureLiteral(" << n << ")\n"; + TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true); if (hasLiteral(n)) { ensureMappingForLiteral(n); @@ -292,7 +295,7 @@ SatLiteral CnfStream::getLiteral(TNode node) { return literal; } -SatLiteral CnfStream::handleXor(TNode xorNode) +void CnfStream::handleXor(TNode xorNode) { Assert(!hasLiteral(xorNode)) << "Atom already mapped!"; Assert(xorNode.getKind() == kind::XOR) << "Expecting an XOR expression!"; @@ -300,8 +303,8 @@ SatLiteral CnfStream::handleXor(TNode xorNode) Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n"; - SatLiteral a = toCNF(xorNode[0]); - SatLiteral b = toCNF(xorNode[1]); + SatLiteral a = getLiteral(xorNode[0]); + SatLiteral b = getLiteral(xorNode[1]); SatLiteral xorLit = newLiteral(xorNode); @@ -309,11 +312,9 @@ SatLiteral CnfStream::handleXor(TNode xorNode) assertClause(xorNode.negate(), ~a, ~b, ~xorLit); assertClause(xorNode, a, ~b, xorLit); assertClause(xorNode, ~a, b, xorLit); - - return xorLit; } -SatLiteral CnfStream::handleOr(TNode orNode) +void CnfStream::handleOr(TNode orNode) { Assert(!hasLiteral(orNode)) << "Atom already mapped!"; Assert(orNode.getKind() == kind::OR) << "Expecting an OR expression!"; @@ -322,37 +323,31 @@ SatLiteral CnfStream::handleOr(TNode orNode) Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n"; // Number of children - unsigned n_children = orNode.getNumChildren(); - - // Transform all the children first - TNode::const_iterator node_it = orNode.begin(); - TNode::const_iterator node_it_end = orNode.end(); - SatClause clause(n_children + 1); - for(int i = 0; node_it != node_it_end; ++node_it, ++i) { - clause[i] = toCNF(*node_it); - } + size_t numChildren = orNode.getNumChildren(); // Get the literal for this node SatLiteral orLit = newLiteral(orNode); - // lit <- (a_1 | a_2 | a_3 | ... | a_n) - // lit | ~(a_1 | a_2 | a_3 | ... | a_n) - // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) - for(unsigned i = 0; i < n_children; ++i) { + // Transform all the children first + SatClause clause(numChildren + 1); + for (size_t i = 0; i < numChildren; ++i) + { + clause[i] = getLiteral(orNode[i]); + + // lit <- (a_1 | a_2 | a_3 | ... | a_n) + // lit | ~(a_1 | a_2 | a_3 | ... | a_n) + // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) assertClause(orNode, orLit, ~clause[i]); } // lit -> (a_1 | a_2 | a_3 | ... | a_n) // ~lit | a_1 | a_2 | a_3 | ... | a_n - clause[n_children] = ~orLit; + clause[numChildren] = ~orLit; // This needs to go last, as the clause might get modified by the SAT solver assertClause(orNode.negate(), clause); - - // Return the literal - return orLit; } -SatLiteral CnfStream::handleAnd(TNode andNode) +void CnfStream::handleAnd(TNode andNode) { Assert(!hasLiteral(andNode)) << "Atom already mapped!"; Assert(andNode.getKind() == kind::AND) << "Expecting an AND expression!"; @@ -361,37 +356,32 @@ SatLiteral CnfStream::handleAnd(TNode andNode) Trace("cnf") << "handleAnd(" << andNode << ")\n"; // Number of children - unsigned n_children = andNode.getNumChildren(); - - // Transform all the children first (remembering the negation) - TNode::const_iterator node_it = andNode.begin(); - TNode::const_iterator node_it_end = andNode.end(); - SatClause clause(n_children + 1); - for(int i = 0; node_it != node_it_end; ++node_it, ++i) { - clause[i] = ~toCNF(*node_it); - } + size_t numChildren = andNode.getNumChildren(); // Get the literal for this node SatLiteral andLit = newLiteral(andNode); - // lit -> (a_1 & a_2 & a_3 & ... & a_n) - // ~lit | (a_1 & a_2 & a_3 & ... & a_n) - // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) - for(unsigned i = 0; i < n_children; ++i) { + // Transform all the children first (remembering the negation) + SatClause clause(numChildren + 1); + for (size_t i = 0; i < numChildren; ++i) + { + clause[i] = ~getLiteral(andNode[i]); + + // lit -> (a_1 & a_2 & a_3 & ... & a_n) + // ~lit | (a_1 & a_2 & a_3 & ... & a_n) + // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) assertClause(andNode.negate(), ~andLit, ~clause[i]); } // lit <- (a_1 & a_2 & a_3 & ... a_n) // lit | ~(a_1 & a_2 & a_3 & ... & a_n) // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n - clause[n_children] = andLit; + clause[numChildren] = andLit; // This needs to go last, as the clause might get modified by the SAT solver assertClause(andNode, clause); - - return andLit; } -SatLiteral CnfStream::handleImplies(TNode impliesNode) +void CnfStream::handleImplies(TNode impliesNode) { Assert(!hasLiteral(impliesNode)) << "Atom already mapped!"; Assert(impliesNode.getKind() == kind::IMPLIES) @@ -401,8 +391,8 @@ SatLiteral CnfStream::handleImplies(TNode impliesNode) Trace("cnf") << "handleImplies(" << impliesNode << ")\n"; // Convert the children to cnf - SatLiteral a = toCNF(impliesNode[0]); - SatLiteral b = toCNF(impliesNode[1]); + SatLiteral a = getLiteral(impliesNode[0]); + SatLiteral b = getLiteral(impliesNode[1]); SatLiteral impliesLit = newLiteral(impliesNode); @@ -415,11 +405,9 @@ SatLiteral CnfStream::handleImplies(TNode impliesNode) // (a | l) & (~b | l) assertClause(impliesNode, a, impliesLit); assertClause(impliesNode, ~b, impliesLit); - - return impliesLit; } -SatLiteral CnfStream::handleIff(TNode iffNode) +void CnfStream::handleIff(TNode iffNode) { Assert(!hasLiteral(iffNode)) << "Atom already mapped!"; Assert(iffNode.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!"; @@ -428,8 +416,8 @@ SatLiteral CnfStream::handleIff(TNode iffNode) Trace("cnf") << "handleIff(" << iffNode << ")\n"; // Convert the children to CNF - SatLiteral a = toCNF(iffNode[0]); - SatLiteral b = toCNF(iffNode[1]); + SatLiteral a = getLiteral(iffNode[0]); + SatLiteral b = getLiteral(iffNode[1]); // Get the now literal SatLiteral iffLit = newLiteral(iffNode); @@ -447,11 +435,9 @@ SatLiteral CnfStream::handleIff(TNode iffNode) // (~a | ~b | lit) & (a | b | lit) assertClause(iffNode, ~a, ~b, iffLit); assertClause(iffNode, a, b, iffLit); - - return iffLit; } -SatLiteral CnfStream::handleIte(TNode iteNode) +void CnfStream::handleIte(TNode iteNode) { Assert(!hasLiteral(iteNode)) << "Atom already mapped!"; Assert(iteNode.getKind() == kind::ITE); @@ -460,9 +446,9 @@ SatLiteral CnfStream::handleIte(TNode iteNode) Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")\n"; - SatLiteral condLit = toCNF(iteNode[0]); - SatLiteral thenLit = toCNF(iteNode[1]); - SatLiteral elseLit = toCNF(iteNode[2]); + SatLiteral condLit = getLiteral(iteNode[0]); + SatLiteral thenLit = getLiteral(iteNode[1]); + SatLiteral elseLit = getLiteral(iteNode[2]); SatLiteral iteLit = newLiteral(iteNode); @@ -485,47 +471,79 @@ SatLiteral CnfStream::handleIte(TNode iteNode) assertClause(iteNode, iteLit, ~thenLit, ~elseLit); assertClause(iteNode, iteLit, ~condLit, ~thenLit); assertClause(iteNode, iteLit, condLit, ~elseLit); - - return iteLit; } SatLiteral CnfStream::toCNF(TNode node, bool negated) { Trace("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")\n"; + + TNode cur; SatLiteral nodeLit; - Node negatedNode = node.notNode(); - - // If the non-negated node has already been translated, get the translation - if(hasLiteral(node)) { - Trace("cnf") << "toCNF(): already translated\n"; - nodeLit = getLiteral(node); - // Return the (maybe negated) literal - return !negated ? nodeLit : ~nodeLit; - } - // Handle each Boolean operator case - switch (node.getKind()) + std::vector<TNode> visit; + std::unordered_map<TNode, bool> cache; + + visit.push_back(node); + while (!visit.empty()) { - case kind::NOT: nodeLit = ~toCNF(node[0]); break; - case kind::XOR: nodeLit = handleXor(node); break; - case kind::ITE: nodeLit = handleIte(node); break; - case kind::IMPLIES: nodeLit = handleImplies(node); break; - case kind::OR: nodeLit = handleOr(node); break; - case kind::AND: nodeLit = handleAnd(node); break; - case kind::EQUAL: - nodeLit = - node[0].getType().isBoolean() ? handleIff(node) : convertAtom(node); - break; - default: + cur = visit.back(); + Assert(cur.getType().isBoolean()); + + if (hasLiteral(cur)) { - nodeLit = convertAtom(node); + visit.pop_back(); + continue; } - break; + + const auto& it = cache.find(cur); + if (it == cache.end()) + { + cache.emplace(cur, false); + Kind k = cur.getKind(); + // Only traverse Boolean nodes + if (k == kind::NOT || k == kind::XOR || k == kind::ITE + || k == kind::IMPLIES || k == kind::OR || k == kind::AND + || (k == kind::EQUAL && cur[0].getType().isBoolean())) + { + // Preserve the order of the recursive version + for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i) + { + visit.push_back(cur[size - 1 - i]); + } + } + continue; + } + else if (!it->second) + { + it->second = true; + Kind k = cur.getKind(); + switch (k) + { + case kind::NOT: Assert(hasLiteral(cur[0])); break; + case kind::XOR: handleXor(cur); break; + case kind::ITE: handleIte(cur); break; + case kind::IMPLIES: handleImplies(cur); break; + case kind::OR: handleOr(cur); break; + case kind::AND: handleAnd(cur); break; + default: + if (k == kind::EQUAL && cur[0].getType().isBoolean()) + { + handleIff(cur); + } + else + { + convertAtom(cur); + } + break; + } + } + visit.pop_back(); } - // Return the (maybe negated) literal + + nodeLit = getLiteral(node); Trace("cnf") << "toCNF(): resulting literal: " << (!negated ? nodeLit : ~nodeLit) << "\n"; - return !negated ? nodeLit : ~nodeLit; + return negated ? ~nodeLit : nodeLit; } void CnfStream::convertAndAssertAnd(TNode node, bool negated) @@ -707,6 +725,7 @@ void CnfStream::convertAndAssert(TNode node, << ", negated = " << (negated ? "true" : "false") << ", removable = " << (removable ? "true" : "false") << ")\n"; d_removable = removable; + TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true); convertAndAssert(node, negated); } @@ -745,5 +764,11 @@ void CnfStream::convertAndAssert(TNode node, bool negated) } } +CnfStream::Statistics::Statistics(const std::string& name) + : d_cnfConversionTime(smtStatisticsRegistry().registerTimer( + name + "::CnfStream::cnfConversionTime")) +{ +} + } // namespace prop } // namespace cvc5 diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 264e26777..aeed97380 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -191,16 +191,16 @@ class CnfStream { */ SatLiteral toCNF(TNode node, bool negated = false); - /** Specific clausifiers, based on the formula kinds, that clausify a formula, - * by calling toCNF into each of the formula's children under the respective - * kind, and introduce a literal definitionally equal to it. */ - SatLiteral handleNot(TNode node); - SatLiteral handleXor(TNode node); - SatLiteral handleImplies(TNode node); - SatLiteral handleIff(TNode node); - SatLiteral handleIte(TNode node); - SatLiteral handleAnd(TNode node); - SatLiteral handleOr(TNode node); + /** + * Specific clausifiers that clausify a formula based on the given formula + * kind and introduce a literal definitionally equal to it. + */ + void handleXor(TNode node); + void handleImplies(TNode node); + void handleIff(TNode node); + void handleIte(TNode node); + void handleAnd(TNode node); + void handleOr(TNode node); /** Stores the literal of the given node in d_literalToNodeMap. * @@ -309,6 +309,14 @@ class CnfStream { /** Pointer to resource manager for associated SmtEngine */ ResourceManager* d_resourceManager; + + private: + struct Statistics + { + Statistics(const std::string& name); + TimerStat d_cnfConversionTime; + } d_stats; + }; /* class CnfStream */ } // namespace prop diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index fd86d3a42..6f99a47f0 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/check.h" #include "base/output.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/prop_options.h" #include "options/smt_options.h" diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 9972581c0..af131c2c3 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -133,7 +133,6 @@ class ProofCnfStream : public ProofGenerator * Specific clausifiers, based on the formula kinds, that clausify a formula, * by calling toCNF into each of the formula's children under the respective * kind, and introduce a literal definitionally equal to it. */ - SatLiteral handleNot(TNode node); SatLiteral handleXor(TNode node); SatLiteral handleImplies(TNode node); SatLiteral handleIff(TNode node); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index fe3a5ecff..62b2f655c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -107,7 +107,8 @@ PropEngine::PropEngine(TheoryEngine* te, userContext, &d_outMgr, rm, - FormulaLitPolicy::TRACK); + FormulaLitPolicy::TRACK, + "prop"); // connect theory proxy d_theoryProxy->finishInit(d_cnfStream); diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 446f72451..0855cbda5 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -53,13 +53,9 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry, SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry, const std::string& name) { -#ifdef CVC5_USE_CADICAL CadicalSolver* res = new CadicalSolver(registry, name); res->init(); return res; -#else - Unreachable() << "cvc5 was not compiled with CaDiCaL support."; -#endif } SatSolver* SatSolverFactory::createKissat(StatisticsRegistry& registry, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index d672b79a6..5f0da7a0c 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -31,6 +31,7 @@ #include "expr/symbol_manager.h" #include "expr/type_node.h" #include "options/options.h" +#include "options/main_options.h" #include "options/printer_options.h" #include "options/smt_options.h" #include "printer/printer.h" diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index e85ea82ef..a46452004 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -32,12 +32,11 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent) : d_parent(parent), d_optChecker(), d_objectives(parent->getUserContext()), - d_results(), - d_objectiveCombination(LEXICOGRAPHIC) + d_results() { } -OptimizationResult::ResultType OptimizationSolver::checkOpt() +Result OptimizationSolver::checkOpt(ObjectiveCombination combination) { // if the results of the previous call have different size than the // objectives, then we should clear the pareto optimization context @@ -48,7 +47,7 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt() { d_results.emplace_back(); } - switch (d_objectiveCombination) + switch (combination) { case BOX: return optimizeBox(); break; case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break; @@ -76,16 +75,9 @@ void OptimizationSolver::addObjective(TNode target, std::vector<OptimizationResult> OptimizationSolver::getValues() { - Assert(d_objectives.size() == d_results.size()); return d_results; } -void OptimizationSolver::setObjectiveCombination( - ObjectiveCombination combination) -{ - d_objectiveCombination = combination; -} - std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout( SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) { @@ -106,13 +98,12 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout( return optChecker; } -OptimizationResult::ResultType OptimizationSolver::optimizeBox() +Result OptimizationSolver::optimizeBox() { // resets the optChecker d_optChecker = createOptCheckerWithTimeout(d_parent); OptimizationResult partialResult; - OptimizationResult::ResultType aggregatedResultType = - OptimizationResult::OPTIMAL; + Result aggregatedResult(Result::Sat::SAT); std::unique_ptr<OMTOptimizer> optimizer; for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { @@ -134,18 +125,19 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox() } // match the optimization result type, and aggregate the results of // subproblems - switch (partialResult.getType()) + switch (partialResult.getResult().isSat()) { - case OptimizationResult::OPTIMAL: break; - case OptimizationResult::UNBOUNDED: break; - case OptimizationResult::UNSAT: - if (aggregatedResultType == OptimizationResult::OPTIMAL) + case Result::SAT: break; + case Result::UNSAT: + // the assertions are unsatisfiable + for (size_t j = 0; j < numObj; ++j) { - aggregatedResultType = OptimizationResult::UNSAT; + d_results[j] = partialResult; } - break; - case OptimizationResult::UNKNOWN: - aggregatedResultType = OptimizationResult::UNKNOWN; + d_optChecker.reset(); + return partialResult.getResult(); + case Result::SAT_UNKNOWN: + aggregatedResult = partialResult.getResult(); break; default: Unreachable(); } @@ -154,15 +146,20 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox() } // kill optChecker after optimization ends d_optChecker.reset(); - return aggregatedResultType; + return aggregatedResult; } -OptimizationResult::ResultType -OptimizationSolver::optimizeLexicographicIterative() +Result OptimizationSolver::optimizeLexicographicIterative() { // resets the optChecker d_optChecker = createOptCheckerWithTimeout(d_parent); - OptimizationResult partialResult; + // partialResult defaults to SAT if no objective is present + // NOTE: the parenthesis around Result(Result::SAT) is required, + // otherwise the compiler will report "parameter declarator cannot be + // qualified". For more details: + // https://stackoverflow.com/questions/44045257/c-compiler-error-c2751-what-exactly-causes-it + // https://en.wikipedia.org/wiki/Most_vexing_parse + OptimizationResult partialResult((Result(Result::SAT)), TNode()); std::unique_ptr<OMTOptimizer> optimizer; for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { @@ -186,26 +183,33 @@ OptimizationSolver::optimizeLexicographicIterative() d_results[i] = partialResult; // checks the optimization result of the current objective - switch (partialResult.getType()) + switch (partialResult.getResult().isSat()) { - case OptimizationResult::OPTIMAL: + case Result::SAT: // assert target[i] == value[i] and proceed d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode( kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue())); break; - case OptimizationResult::UNBOUNDED: return OptimizationResult::UNBOUNDED; - case OptimizationResult::UNSAT: return OptimizationResult::UNSAT; - case OptimizationResult::UNKNOWN: return OptimizationResult::UNKNOWN; + case Result::UNSAT: + d_optChecker.reset(); + return partialResult.getResult(); + case Result::SAT_UNKNOWN: + d_optChecker.reset(); + return partialResult.getResult(); default: Unreachable(); } + + // if the result for the current objective is unbounded + // then just stop + if (partialResult.isUnbounded()) break; } // kill optChecker in case pareto misuses it d_optChecker.reset(); - // now all objectives are OPTIMAL, just return OPTIMAL as overall result - return OptimizationResult::OPTIMAL; + // now all objectives are optimal, just return SAT as the overall result + return partialResult.getResult(); } -OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() +Result OptimizationSolver::optimizeParetoNaiveGIA() { // initial call to Pareto optimizer, create the checker if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent); @@ -216,8 +220,8 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() switch (satResult.isSat()) { - case Result::Sat::UNSAT: return OptimizationResult::UNSAT; - case Result::Sat::SAT_UNKNOWN: return OptimizationResult::UNKNOWN; + case Result::Sat::UNSAT: return satResult; + case Result::Sat::SAT_UNKNOWN: return satResult; case Result::Sat::SAT: { // if satisfied, use d_results to store the initial results @@ -226,14 +230,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { d_results[i] = OptimizationResult( - OptimizationResult::OPTIMAL, - d_optChecker->getValue(d_objectives[i].getTarget())); + satResult, d_optChecker->getValue(d_objectives[i].getTarget())); } break; } default: Unreachable(); } + Result lastSatResult = satResult; + // a vector storing assertions saying that no objective is worse std::vector<Node> noWorseObj; // a vector storing assertions saying that there is at least one objective @@ -278,15 +283,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() case Result::Sat::SAT_UNKNOWN: // if result is UNKNOWN, abort the current session and return UNKNOWN d_optChecker.reset(); - return OptimizationResult::UNKNOWN; + return satResult; case Result::Sat::SAT: { + lastSatResult = satResult; // if result is SAT, update d_results to the more optimal values for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { d_results[i] = OptimizationResult( - OptimizationResult::OPTIMAL, - d_optChecker->getValue(d_objectives[i].getTarget())); + satResult, d_optChecker->getValue(d_objectives[i].getTarget())); } break; } @@ -302,7 +307,7 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() // for the next run. d_optChecker->assertFormula(nm->mkOr(someObjBetter)); - return OptimizationResult::OPTIMAL; + return lastSatResult; } } // namespace smt diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 6d138deb2..d13168780 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -33,63 +33,75 @@ namespace smt { /** * The optimization result of an optimization objective * containing: - * - whether it's optimal or not - * - if so, the optimal value, otherwise the value might be empty node or - * something suboptimal + * - the optimization result: SAT/UNSAT/UNKNOWN + * - the optimal value if SAT and bounded + * (optimal value reached and it's not infinity), + * or an empty node if SAT and unbounded + * (optimal value is +inf for maximum or -inf for minimum), + * otherwise the value might be empty node + * or something suboptimal + * - whether the objective is unbounded */ class OptimizationResult { public: /** - * Enum indicating whether the checkOpt result - * is optimal or not. - **/ - enum ResultType - { - // whether the value is optimal is UNKNOWN - UNKNOWN, - // the original set of assertions has result UNSAT - UNSAT, - // the value is optimal - OPTIMAL, - // the goal is unbounded, - // if objective is maximize, it's +infinity - // if objective is minimize, it's -infinity - UNBOUNDED, - }; - - /** * Constructor * @param type the optimization outcome * @param value the optimized value + * @param unbounded whether the objective is unbounded **/ - OptimizationResult(ResultType type, TNode value) - : d_type(type), d_value(value) + OptimizationResult(Result result, TNode value, bool unbounded = false) + : d_result(result), d_value(value), d_unbounded(unbounded) + { + } + OptimizationResult() + : d_result(Result::Sat::SAT_UNKNOWN, + Result::UnknownExplanation::NO_STATUS), + d_value(), + d_unbounded(false) { } - OptimizationResult() : d_type(UNKNOWN), d_value() {} ~OptimizationResult() = default; /** * Returns an enum indicating whether - * the result is optimal or not. - * @return an enum showing whether the result is optimal, unbounded, - * unsat or unknown. + * the result is SAT or not. + * @return whether the result is SAT, UNSAT or SAT_UNKNOWN **/ - ResultType getType() const { return d_type; } + Result getResult() const { return d_result; } + /** * Returns the optimal value. * @return Node containing the optimal value, - * if getType() is not OPTIMAL, it might return an empty node or a node - * containing non-optimal value + * if result is unbounded, this will be an empty node, + * if getResult() is UNSAT, it will return an empty node, + * if getResult() is SAT_UNKNOWN, it will return something suboptimal + * or an empty node, depending on how the solver runs. **/ Node getValue() const { return d_value; } + /** + * Checks whether the objective is unbouned + * @return whether the objective is unbounded + * if the objective is unbounded (this function returns true), + * then the optimal value is: + * +inf, if it's maximize; + * -inf, if it's minimize + **/ + bool isUnbounded() const { return d_unbounded; } + private: - /** the indicating whether the result is optimal or something else **/ - ResultType d_type; - /** if the result is optimal, this is storing the optimal value **/ + /** indicating whether the result is SAT, UNSAT or UNKNOWN **/ + Result d_result; + /** if the result is bounded, this is storing the value **/ Node d_value; + /** whether the objective is unbounded + * If this is true, then: + * if objective is maximize, it's +infinity; + * if objective is minimize, it's -infinity + **/ + bool d_unbounded; }; /** @@ -199,10 +211,10 @@ class OptimizationSolver /** * Run the optimization loop for the added objective * For multiple objective combination, it defaults to lexicographic, - * and combination could be set by calling - * setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO) + * possible combinations: BOX, LEXICOGRAPHIC, PARETO + * @param combination BOX / LEXICOGRAPHIC / PARETO */ - OptimizationResult::ResultType checkOpt(); + Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC); /** * Add an optimization objective. @@ -223,11 +235,6 @@ class OptimizationSolver **/ std::vector<OptimizationResult> getValues(); - /** - * Sets the objective combination - **/ - void setObjectiveCombination(ObjectiveCombination combination); - private: /** * Initialize an SMT subsolver for offline optimization purpose @@ -244,26 +251,26 @@ class OptimizationSolver /** * Optimize multiple goals in Box order - * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED; - * UNSAT if at least one objective is UNSAT and no objective is UNKNOWN; - * UNKNOWN if any of the objective is UNKNOWN. + * @return SAT if all of the objectives are optimal or unbounded; + * UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN; + * SAT_UNKNOWN if any of the objective is SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeBox(); + Result optimizeBox(); /** * Optimize multiple goals in Lexicographic order, * using iterative implementation - * @return OPTIMAL if all objectives are OPTIMAL and bounded; - * UNBOUNDED if one of the objectives is UNBOUNDED + * @return SAT if the objectives are optimal, + * if one of the objectives is unbounded, + * the optimization will stop at that objective; + * UNSAT if any of the objectives is UNSAT * and optimization will stop at that objective; - * UNSAT if one of the objectives is UNSAT - * and optimization will stop at that objective; - * UNKNOWN if one of the objectives is UNKNOWN + * SAT_UNKNOWN if any of the objectives is UNKNOWN * and optimization will stop at that objective; * If the optimization is stopped at an objective, - * all objectives following that objective will be UNKNOWN. + * all objectives following that objective will be SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeLexicographicIterative(); + Result optimizeLexicographicIterative(); /** * Optimize multiple goals in Pareto order @@ -277,11 +284,12 @@ class OptimizationSolver * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm. * Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009. * - * @return if it finds a new Pareto optimal result it will return OPTIMAL; + * @return if it finds a new Pareto optimal result it will return SAT; * if it exhausts the results in the Pareto front it will return UNSAT; - * if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN. + * if the underlying SMT solver returns SAT_UNKNOWN, + * it will return SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeParetoNaiveGIA(); + Result optimizeParetoNaiveGIA(); /** A pointer to the parent SMT engine **/ SmtEngine* d_parent; @@ -294,9 +302,6 @@ class OptimizationSolver /** The results of the optimizations from the last checkOpt call **/ std::vector<OptimizationResult> d_results; - - /** The current objective combination method **/ - ObjectiveCombination d_objectiveCombination; }; } // namespace smt diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 7406b922e..3c0a4ac5b 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -15,6 +15,7 @@ #include "smt/preprocessor.h" +#include "options/base_options.h" #include "options/expr_options.h" #include "options/smt_options.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index cd05b84c4..e119ce4d4 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -66,7 +66,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // unsat cores and proofs shenanigans if (options::dumpUnsatCoresFull()) { - opts.smt.dumpUnsatCores = true; + opts.driver.dumpUnsatCores = true; } if (options::checkUnsatCores() || options::dumpUnsatCores() || options::unsatAssumptions() diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bd48fe0ea..9056e7c94 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -29,7 +29,6 @@ #include "options/option_exception.h" #include "options/printer_options.h" #include "options/proof_options.h" -#include "options/resource_manager_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" @@ -1811,16 +1810,16 @@ void SmtEngine::setResourceLimit(uint64_t units, bool cumulative) { if (cumulative) { - d_env->d_options.resman.cumulativeResourceLimit = units; + d_env->d_options.base.cumulativeResourceLimit = units; } else { - d_env->d_options.resman.perCallResourceLimit = units; + d_env->d_options.base.perCallResourceLimit = units; } } void SmtEngine::setTimeLimit(uint64_t millis) { - d_env->d_options.resman.perCallMillisecondLimit = millis; + d_env->d_options.base.perCallMillisecondLimit = millis; } unsigned long SmtEngine::getResourceUsage() const diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 4afa15a3b..cb0a94123 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -16,6 +16,7 @@ #include "smt/smt_engine_state.h" #include "base/modal_exception.h" +#include "options/base_options.h" #include "options/option_exception.h" #include "options/smt_options.h" #include "smt/smt_engine.h" diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index 417d345cb..c76a8a2e7 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -25,8 +25,6 @@ SmtEngineStatistics::SmtEngineStatistics(const std::string& name) name + "definitionExpansionTime")), d_numConstantProps( smtStatisticsRegistry().registerInt(name + "numConstantProps")), - d_cnfConversionTime( - smtStatisticsRegistry().registerTimer(name + "cnfConversionTime")), d_numAssertionsPre(smtStatisticsRegistry().registerInt( name + "numAssertionsPreITERemoval")), d_numAssertionsPost(smtStatisticsRegistry().registerInt( diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index 441721a54..db914b560 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -30,8 +30,6 @@ struct SmtEngineStatistics TimerStat d_definitionExpansionTime; /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; - /** time spent converting to CNF */ - TimerStat d_cnfConversionTime; /** Number of assertions before ite removal */ IntStat d_numAssertionsPre; /** Number of assertions after ite removal */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index d7b70f501..f5783ab6b 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -239,7 +239,6 @@ void SmtSolver::processAssertions(Assertions& as) // Push the formula to SAT { Chat() << "converting to CNF..." << endl; - TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime); const std::vector<Node>& assertions = ap.ref(); // It is important to distinguish the input assertions from the skolem // definitions, as the decision justification heuristic treates the latter diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 8fa610cda..98278ef9e 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -20,6 +20,7 @@ #include "base/modal_exception.h" #include "expr/dtype.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" #include "options/option_exception.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 99b95719f..3dff64113 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -22,6 +22,7 @@ #include "base/output.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" #include "options/smt_options.h" #include "preprocessing/util/ite_utilities.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 396befb35..0c93db90f 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -26,6 +26,7 @@ operator INTS_MODULUS_TOTAL 2 "integer modulus with interpreted division by 0 (i operator ABS 1 "absolute value" parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term" operator POW 2 "arithmetic power" +operator POW2 1 "arithmetic power of 2" operator EXPONENTIAL 1 "exponential" operator SINE 1 "sine" @@ -148,6 +149,7 @@ typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>" typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>" typerule ARCSECANT "SimpleTypeRule<RReal, AReal>" typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>" +typerule POW2 "SimpleTypeRule<RInteger, AInteger>" typerule SQRT "SimpleTypeRule<RReal, AReal>" diff --git a/src/theory/arith/nl/cad/lazard_evaluation.cpp b/src/theory/arith/nl/cad/lazard_evaluation.cpp index 82b127ed0..2fee21cbf 100644 --- a/src/theory/arith/nl/cad/lazard_evaluation.cpp +++ b/src/theory/arith/nl/cad/lazard_evaluation.cpp @@ -1,5 +1,7 @@ #include "theory/arith/nl/cad/lazard_evaluation.h" +#ifdef CVC5_POLY_IMP + #include "base/check.h" #include "base/output.h" @@ -44,3 +46,5 @@ std::vector<poly::Interval> LazardEvaluation::infeasibleRegions( } } // namespace cvc5::theory::arith::nl::cad + +#endif diff --git a/src/theory/arith/nl/cad/lazard_evaluation.h b/src/theory/arith/nl/cad/lazard_evaluation.h index 0edb12010..3bb971c4c 100644 --- a/src/theory/arith/nl/cad/lazard_evaluation.h +++ b/src/theory/arith/nl/cad/lazard_evaluation.h @@ -19,6 +19,8 @@ #ifndef CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H #define CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H +#ifdef CVC5_POLY_IMP + #include <poly/polyxx.h> #include <memory> @@ -106,4 +108,5 @@ class LazardEvaluation } // namespace cvc5::theory::arith::nl::cad -#endif
\ No newline at end of file +#endif +#endif diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp new file mode 100644 index 000000000..534895c7f --- /dev/null +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -0,0 +1,73 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Makai Mann, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of pow2 solver. + */ + +#include "theory/arith/nl/pow2_solver.h" + +#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_state.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace arith { +namespace nl { + +Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model) + : d_im(im), d_model(model), d_initRefine(state.getUserContext()) +{ + NodeManager* nm = NodeManager::currentNM(); + d_false = nm->mkConst(false); + d_true = nm->mkConst(true); + d_zero = nm->mkConst(Rational(0)); + d_one = nm->mkConst(Rational(1)); + d_two = nm->mkConst(Rational(2)); +} + +Pow2Solver::~Pow2Solver() {} + +void Pow2Solver::initLastCall(const std::vector<Node>& assertions, + const std::vector<Node>& false_asserts, + const std::vector<Node>& xts) +{ + d_pow2s.clear(); + Trace("pow2-mv") << "POW2 terms : " << std::endl; + for (const Node& a : xts) + { + Kind ak = a.getKind(); + if (ak != POW2) + { + // don't care about other terms + continue; + } + d_pow2s.push_back(a); + } + Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl; +} + +void Pow2Solver::checkInitialRefine() {} + +void Pow2Solver::checkFullRefine() {} + +Node Pow2Solver::valueBasedLemma(Node i) { return Node(); } + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index a675c1bf4..97b29b6b3 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -35,7 +35,7 @@ #include "expr/node_builder.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" -#include "options/smt_options.h" // for incrementalSolving() +#include "options/base_options.h" #include "preprocessing/util/ite_utilities.h" #include "proof/proof_generator.h" #include "proof/proof_node_manager.h" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index ea18b3180..be8e1a08e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -151,6 +151,8 @@ bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; esi.d_name = d_instanceName + "ee"; + esi.d_notifyNewClass = true; + esi.d_notifyMerge = true; return true; } diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 9871f2a92..55ed6c41d 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -16,6 +16,7 @@ #include "theory/bv/bitblast/eager_bitblaster.h" #include "cvc5_private.h" +#include "options/base_options.h" #include "options/bv_options.h" #include "options/smt_options.h" #include "prop/cnf_stream.h" diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp index a38dfdfe5..357a54b1a 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.cpp +++ b/src/theory/bv/bitblast/simple_bitblaster.cpp @@ -17,6 +17,7 @@ #include "theory/theory_model.h" #include "theory/theory_state.h" +#include "options/bv_options.h" namespace cvc5 { namespace theory { @@ -129,6 +130,15 @@ Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel) return utils::mkConst(bits.size(), value); } +void BBSimple::computeRelevantTerms(std::set<Node>& termSet) +{ + Assert(options::bitblastMode() == options::BitblastMode::EAGER); + for (const auto& var : d_variables) + { + termSet.insert(var); + } +} + bool BBSimple::collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms) { diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h index ebbb2891f..ec0899145 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.h +++ b/src/theory/bv/bitblast/simple_bitblaster.h @@ -53,6 +53,8 @@ class BBSimple : public TBitblaster<Node> /** Create 'bits' for variable 'var'. */ void makeVariable(TNode var, Bits& bits) override; + /** Add d_variables to termSet. */ + void computeRelevantTerms(std::set<Node>& termSet); /** Collect model values for all relevant terms given in 'relevantTerms'. */ bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms); diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 2d0ae1931..b0082b992 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -15,6 +15,7 @@ #include "theory/bv/bv_eager_solver.h" +#include "options/base_options.h" #include "options/bv_options.h" #include "options/smt_options.h" #include "theory/bv/bitblast/aig_bitblaster.h" diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index 8ff4318c0..6ccc6c7c1 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -32,7 +32,7 @@ class BVSolver BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr) : d_state(state), d_im(inferMgr){}; - virtual ~BVSolver(){}; + virtual ~BVSolver() {} /** * Returns true if we need an equality engine. If so, we initialize the @@ -71,7 +71,7 @@ class BVSolver virtual bool needsCheckLastEffort() { return false; } - virtual void propagate(Theory::Effort e){}; + virtual void propagate(Theory::Effort e) {} virtual TrustNode explain(TNode n) { @@ -80,17 +80,20 @@ class BVSolver return TrustNode::null(); } + /** Additionally collect terms relevant for collecting model values. */ + virtual void computeRelevantTerms(std::set<Node>& termSet) {} + /** Collect model values in m based on the relevant terms given by termSet */ virtual bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) = 0; virtual std::string identify() const = 0; - virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }; + virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); } - virtual void ppStaticLearn(TNode in, NodeBuilder& learned){}; + virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {} - virtual void presolve(){}; + virtual void presolve() {} virtual void notifySharedTerm(TNode t) {} diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index dc2c7e2a3..3ae4a7f0a 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -96,17 +96,19 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, { case options::SatSolverMode::CRYPTOMINISAT: d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( - smtStatisticsRegistry(), "theory::bv::BVSolverBitblast")); + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); break; default: d_satSolver.reset(prop::SatSolverFactory::createCadical( - smtStatisticsRegistry(), "theory::bv::BVSolverBitblast")); + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); } d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), d_bbRegistrar.get(), d_nullContext.get(), nullptr, - smt::currentResourceManager())); + smt::currentResourceManager(), + prop::FormulaLitPolicy::INTERNAL, + "theory::bv::BVSolverBitblast")); } void BVSolverBitblast::postCheck(Theory::Effort level) @@ -236,6 +238,21 @@ TrustNode BVSolverBitblast::explain(TNode n) return d_im.explainLit(n); } +void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet) +{ + /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain + * equalities. As a result, these equalities are not handled by the equality + * engine and terms below these equalities do not appear in `termSet`. + * We need to make sure that we compute model values for all relevant terms + * in BitblastMode::EAGER and therefore add all variables from the + * bit-blaster to `termSet`. + */ + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + d_bitblaster->computeRelevantTerms(termSet); + } +} + bool BVSolverBitblast::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 31d9443c8..c5134c6fc 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -64,6 +64,8 @@ class BVSolverBitblast : public BVSolver EqualityStatus getEqualityStatus(TNode a, TNode b) override; + void computeRelevantTerms(std::set<Node>& termSet) override; + bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp new file mode 100644 index 000000000..9da9d1c2b --- /dev/null +++ b/src/theory/bv/int_blaster.cpp @@ -0,0 +1,240 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Int-blasting utility + */ + +#include "theory/bv/int_blaster.h" + +#include <cmath> +#include <string> +#include <unordered_map> +#include <vector> + +#include "expr/node.h" +#include "expr/node_traversal.h" +#include "expr/skolem_manager.h" +#include "options/option_exception.h" +#include "options/uf_options.h" +#include "theory/rewriter.h" +#include "util/iand.h" +#include "util/rational.h" + +namespace cvc5 { +using namespace cvc5::theory; + +IntBlaster::IntBlaster(context::Context* c, + options::SolveBVAsIntMode mode, + uint64_t granularity, + bool introduceFreshIntVars) + : d_binarizeCache(c), + d_intblastCache(c), + d_rangeAssertions(c), + d_bitwiseAssertions(c), + d_mode(mode), + d_granularity(granularity), + d_context(c), + d_introduceFreshIntVars(introduceFreshIntVars) +{ + d_nm = NodeManager::currentNM(); + d_zero = d_nm->mkConst<Rational>(0); + d_one = d_nm->mkConst<Rational>(1); +}; + +void IntBlaster::addRangeConstraint(Node node, + uint64_t size, + std::vector<Node>& lemmas) +{ +} + +void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint, + std::vector<Node>& lemmas) +{ +} + +Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); } + +Node IntBlaster::maxInt(uint64_t k) { return Node(); } + +Node IntBlaster::pow2(uint64_t k) { return Node(); } + +Node IntBlaster::modpow2(Node n, uint64_t exponent) { return Node(); } + +Node IntBlaster::makeBinary(Node n) +{ + if (d_binarizeCache.find(n) != d_binarizeCache.end()) + { + return d_binarizeCache[n]; + } + uint64_t numChildren = n.getNumChildren(); + kind::Kind_t k = n.getKind(); + Node result = n; + if ((numChildren > 2) + && (k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT + || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR + || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT)) + { + result = n[0]; + for (uint64_t i = 1; i < numChildren; i++) + { + result = d_nm->mkNode(n.getKind(), result, n[i]); + } + } + d_binarizeCache[n] = result; + Trace("int-blaster-debug") << "binarization result: " << result << std::endl; + return result; +} + +/** + * Translate n to Integers via post-order traversal. + */ +Node IntBlaster::intBlast(Node n, + std::vector<Node>& lemmas, + std::map<Node, Node>& skolems) +{ + // make sure the node is re-written + n = Rewriter::rewrite(n); + + // helper vector for traversal. + std::vector<Node> toVisit; + toVisit.push_back(makeBinary(n)); + + while (!toVisit.empty()) + { + Node current = toVisit.back(); + uint64_t currentNumChildren = current.getNumChildren(); + if (d_intblastCache.find(current) == d_intblastCache.end()) + { + // This is the first time we visit this node and it is not in the cache. + // We mark this node as visited but not translated by assiging + // a null node to it. + d_intblastCache[current] = Node(); + // all the node's children are added to the stack to be visited + // before visiting this node again. + for (const Node& child : current) + { + toVisit.push_back(makeBinary(child)); + } + // If this is a UF applicatinon, we also add the function to + // toVisit. + if (current.getKind() == kind::APPLY_UF) + { + toVisit.push_back(current.getOperator()); + } + } + else + { + // We already visited and translated this node + if (!d_intblastCache[current].get().isNull()) + { + // We are done computing the translation for current + toVisit.pop_back(); + } + else + { + // We are now visiting current on the way back up. + // This is when we do the actual translation. + Node translation; + if (currentNumChildren == 0) + { + translation = translateNoChildren(current, lemmas, skolems); + } + else + { + /** + * The current node has children. + * Since we are on the way back up, + * these children were already translated. + * We save their translation for easy access. + * If the node's kind is APPLY_UF, + * we also need to include the translated uninterpreted function in + * this list. + */ + std::vector<Node> translated_children; + if (current.getKind() == kind::APPLY_UF) + { + translated_children.push_back( + d_intblastCache[current.getOperator()]); + } + for (uint64_t i = 0; i < currentNumChildren; i++) + { + translated_children.push_back(d_intblastCache[current[i]]); + } + translation = + translateWithChildren(current, translated_children, lemmas); + } + + Assert(!translation.isNull()); + // Map the current node to its translation in the cache. + d_intblastCache[current] = translation; + // Also map the translation to itself. + d_intblastCache[translation] = translation; + toVisit.pop_back(); + } + } + } + return d_intblastCache[n].get(); +} + +Node IntBlaster::unsignedToSigned(Node n, uint64_t bw) { return Node(); } + +Node IntBlaster::translateWithChildren( + Node original, + const std::vector<Node>& translated_children, + std::vector<Node>& lemmas) +{ + Node binarized = makeBinary(original); + // continue to process the binarized version + return Node(); +} + +Node IntBlaster::translateNoChildren(Node original, + std::vector<Node>& lemmas, + std::map<Node, Node>& skolems) +{ + return Node(); +} + +Node IntBlaster::defineBVUFAsIntUF(Node bvUF, Node intUF) { return Node(); } + +Node IntBlaster::translateFunctionSymbol(Node bvUF, + std::map<Node, Node>& skolems) +{ + return Node(); +} + +bool IntBlaster::childrenTypesChanged(Node n) { return true; } + +Node IntBlaster::castToType(Node n, TypeNode tn) { return Node(); } + +Node IntBlaster::reconstructNode(Node originalNode, + TypeNode resultType, + const std::vector<Node>& translated_children) +{ + return Node(); +} + +Node IntBlaster::createShiftNode(std::vector<Node> children, + uint64_t bvsize, + bool isLeftShift) +{ + return Node(); +} + +Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode) +{ + return Node(); +} + +Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) { return Node(); } + +} // namespace cvc5 diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h index f8717e045..444eb88a7 100644 --- a/src/theory/bv/int_blaster.h +++ b/src/theory/bv/int_blaster.h @@ -75,9 +75,10 @@ namespace cvc5 { ** Tr((bvult a b)) = Tr(a) < Tr(b) ** Similar transformations are done for bvule, bvugt, and bvuge. ** -** Bit-vector operators that are not listed above are either eliminated using -** the function eliminationPass, or go through the following default -*translation, that also works for non-bit-vector operators +** Bit-vector operators that are not listed above are either +** eliminated using the BV rewriter, +** or go through the following default +** translation, that also works for non-bit-vector operators ** with result type BV: ** Tr((op t1 ... tn)) = (bv2nat (op (cast t1) ... (cast tn))) ** where (cast x) is ((_ nat2bv k) x) or just x, @@ -118,8 +119,7 @@ class IntBlaster * ff((bv2nat x))), where k is the bit-width of the domain of f, i is the * bit-width of its range, and ff is a Int->Int function that corresponds to * f. For functions with other signatures this is similar - * @return integer node that corresponds to n, or a null node if d_supportNoBV - * is set to false and n is note purely BV. + * @return integer node that corresponds to n */ Node intBlast(Node n, std::vector<Node>& lemmas, @@ -165,18 +165,15 @@ class IntBlaster Node mkRangeConstraint(Node newVar, uint64_t k); /** - * In the translation to integers, it is convenient to assume that certain - * bit-vector operators do not occur in the original formula (e.g., repeat). - * This function eliminates all these operators. - */ - Node eliminationPass(Node n); - - /** * Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more * than two arguments as a syntactic sugar. * For example, we can have a node for (bvand x y z), * that represents (bvand (x (bvand y z))). - * This function makes all such operators strictly binary. + * This function locally binarizes these operators. + * In the above example, this means that x,y,z + * are not handled recursively, but will require a separate + * call to the function. + * */ Node makeBinary(Node n); @@ -287,7 +284,7 @@ class IntBlaster * binary representation of n is the same as the * signed binary representation of m. */ - Node unsignedTosigned(Node n, uint64_t bvsize); + Node unsignedToSigned(Node n, uint64_t bvsize); /** * Performs the actual translation to integers for nodes @@ -308,8 +305,6 @@ class IntBlaster /** Caches for the different functions */ CDNodeMap d_binarizeCache; - CDNodeMap d_eliminationCache; - CDNodeMap d_rebuildCache; CDNodeMap d_intblastCache; /** Node manager that is used throughout the pass */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 22b05b026..3d7f11f6d 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -175,6 +175,11 @@ bool TheoryBV::needsCheckLastEffort() return d_internal->needsCheckLastEffort(); } +void TheoryBV::computeRelevantTerms(std::set<Node>& termSet) +{ + return d_internal->computeRelevantTerms(termSet); +} + bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { return d_internal->collectModelValues(m, termSet); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 4b3a1f3b2..e884f621c 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -83,6 +83,8 @@ class TheoryBV : public Theory TrustNode explain(TNode n) override; + void computeRelevantTerms(std::set<Node>& termSet) override; + /** Collect model values in m based on the relevant terms given by termSet */ bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index dc57e4165..53f128286 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -94,6 +94,9 @@ bool TheoryDatatypes::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; esi.d_name = "theory::datatypes::ee"; + // need notifications on new constructors, merging datatype eqcs + esi.d_notifyNewClass = true; + esi.d_notifyMerge = true; return true; } diff --git a/src/theory/ee_setup_info.h b/src/theory/ee_setup_info.h index f6139d109..130241c4a 100644 --- a/src/theory/ee_setup_info.h +++ b/src/theory/ee_setup_info.h @@ -39,7 +39,12 @@ class EqualityEngineNotify; struct EeSetupInfo { EeSetupInfo() - : d_notify(nullptr), d_constantsAreTriggers(true), d_useMaster(false) + : d_notify(nullptr), + d_constantsAreTriggers(true), + d_notifyNewClass(false), + d_notifyMerge(false), + d_notifyDisequal(false), + d_useMaster(false) { } /** The notification class of the theory */ @@ -48,11 +53,25 @@ struct EeSetupInfo std::string d_name; /** Constants are triggers */ bool d_constantsAreTriggers; + //-------------------------- fine grained notifications + /** Whether we need to be notified of new equivalence classes */ + bool d_notifyNewClass; + /** Whether we need to be notified of merged equivalence classes */ + bool d_notifyMerge; + /** Whether we need to be notified of disequal equivalence classes */ + bool d_notifyDisequal; + //-------------------------- end fine grained notifications /** * Whether we want our state to use the master equality engine. This should * be true exclusively for the theory of quantifiers. */ bool d_useMaster; + /** Does it need notifications when equivalence classes are created? */ + bool needsNotifyNewClass() const { return d_notifyNewClass; } + /** Does it need notifications when equivalence classes are merged? */ + bool needsNotifyMerge() const { return d_notifyMerge; } + /** Does it need notifications when disequalities are generated? */ + bool needsNotifyDisequal() const { return d_notifyDisequal; } }; } // namespace theory diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 0d1b25549..0e196c0e0 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -23,7 +23,6 @@ #include "util/floatingpoint.h" #include "util/floatingpoint_literal_symfpu.h" -#ifdef CVC5_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" #include "symfpu/core/compare.h" @@ -38,9 +37,7 @@ #include "symfpu/core/sqrt.h" #include "symfpu/utils/numberOfRoundingModes.h" #include "symfpu/utils/properties.h" -#endif -#ifdef CVC5_USE_SYMFPU namespace symfpu { using namespace ::cvc5::theory::fp::symfpuSymbolic; @@ -143,11 +140,6 @@ void probabilityAnnotation<traits, traits::prop>(const traits::prop &p, return; } }; -#endif - -#ifndef CVC5_USE_SYMFPU -#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5 -#endif namespace cvc5 { namespace theory { @@ -242,11 +234,7 @@ symbolicProposition symbolicProposition::operator^( bool symbolicRoundingMode::checkNodeType(const TNode n) { -#ifdef CVC5_USE_SYMFPU return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES); -#else - return false; -#endif } symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n) @@ -254,7 +242,6 @@ symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n) Assert(checkNodeType(*this)); } -#ifdef CVC5_USE_SYMFPU symbolicRoundingMode::symbolicRoundingMode(const unsigned v) : nodeWrapper(NodeManager::currentNM()->mkConst( BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) @@ -262,14 +249,6 @@ symbolicRoundingMode::symbolicRoundingMode(const unsigned v) Assert((v & (v - 1)) == 0 && v != 0); // Exactly one bit set Assert(checkNodeType(*this)); } -#else -symbolicRoundingMode::symbolicRoundingMode(const unsigned v) - : nodeWrapper(NodeManager::currentNM()->mkConst( - BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) -{ - Unreachable(); -} -#endif symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old) : nodeWrapper(old) @@ -755,20 +734,17 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const FpConverter::FpConverter(context::UserContext* user) : d_additionalAssertions(user) -#ifdef CVC5_USE_SYMFPU , d_fpMap(user), d_rmMap(user), d_boolMap(user), d_ubvMap(user), d_sbvMap(user) -#endif { } FpConverter::~FpConverter() {} -#ifdef CVC5_USE_SYMFPU Node FpConverter::ufToNode(const fpt &format, const uf &u) const { NodeManager *nm = NodeManager::currentNM(); @@ -843,7 +819,6 @@ FpConverter::uf FpConverter::buildComponents(TNode current) return tmp; } -#endif // Non-convertible things should only be added to the stack at the very start, // thus... @@ -851,7 +826,6 @@ FpConverter::uf FpConverter::buildComponents(TNode current) Node FpConverter::convert(TNode node) { -#ifdef CVC5_USE_SYMFPU std::vector<TNode> workStack; TNode result = node; @@ -1704,9 +1678,6 @@ Node FpConverter::convert(TNode node) } return result; -#else - Unimplemented() << "Conversion is dependent on SymFPU"; -#endif } #undef CVC5_FPCONV_PASSTHROUGH @@ -1715,7 +1686,6 @@ Node FpConverter::getValue(Valuation &val, TNode var) { Assert(Theory::isLeafOf(var, THEORY_FP)); -#ifdef CVC5_USE_SYMFPU TypeNode t(var.getType()); Assert(t.isRoundingMode() || t.isFloatingPoint()) @@ -1735,9 +1705,6 @@ Node FpConverter::getValue(Valuation &val, TNode var) Assert(i != d_fpMap.end()) << "Asking for the value of an unregistered expression"; return ufToNode(fpt(t), (*i).second); -#else - Unimplemented() << "Conversion is dependent on SymFPU"; -#endif } } // namespace fp diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index f1b7c8a83..9900c2987 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -33,9 +33,7 @@ #include "util/floatingpoint_size.h" #include "util/hash.h" -#ifdef CVC5_USE_SYMFPU #include "symfpu/core/unpackedFloat.h" -#endif #ifdef CVC5_SYM_SYMBOLIC_EVAL // This allows debugging of the cvc5 symbolic back-end. @@ -120,9 +118,7 @@ class symbolicProposition : public nodeWrapper protected: bool checkNodeType(const TNode node); -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE -#endif public: symbolicProposition(const Node n); @@ -141,9 +137,7 @@ class symbolicRoundingMode : public nodeWrapper protected: bool checkNodeType(const TNode n); -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE -#endif public: symbolicRoundingMode(const Node n); @@ -183,10 +177,8 @@ class symbolicBitVector : public nodeWrapper bool checkNodeType(const TNode n); friend symbolicBitVector<!isSigned>; // To allow conversion between the types -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicBitVector<isSigned> >; // For ITE -#endif public: symbolicBitVector(const Node n); @@ -314,7 +306,6 @@ class FpConverter context::CDList<Node> d_additionalAssertions; protected: -#ifdef CVC5_USE_SYMFPU typedef symfpuSymbolic::traits traits; typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf; typedef symfpuSymbolic::traits::rm rm; @@ -348,7 +339,6 @@ class FpConverter /* Creates the relevant components for a variable */ uf buildComponents(TNode current); -#endif }; } // namespace fp diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 3d81a2995..77dba0724 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -661,7 +661,7 @@ bool TheoryFp::isRegistered(TNode node) { void TheoryFp::preRegisterTerm(TNode node) { - if (Configuration::isBuiltWithSymFPU() && !options::fpExp()) + if (!options::fpExp()) { TypeNode tn = node.getType(); if (tn.isFloatingPoint()) diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 76f7d55cf..8bc7900de 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -1026,12 +1026,10 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) bool result; switch (k) { -#ifdef CVC5_USE_SYMFPU case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break; case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break; case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break; case kind::FLOATINGPOINT_COMPONENT_SIGN: result = arg0.getSign(); break; -#endif default: Unreachable() << "Unknown kind used in componentFlag"; break; } @@ -1050,11 +1048,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) // \todo Add a proper interface for this sort of thing to FloatingPoint #1915 return RewriteResponse( REWRITE_DONE, -#ifdef CVC5_USE_SYMFPU NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent()) -#else - node -#endif ); } @@ -1066,11 +1060,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) return RewriteResponse( REWRITE_DONE, -#ifdef CVC5_USE_SYMFPU NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand()) -#else - node -#endif ); } @@ -1080,7 +1070,6 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) BitVector value; -#ifdef CVC5_USE_SYMFPU /* \todo fix the numbering of rounding modes so this doesn't need * to call symfpu at all and remove the dependency on fp_converter.h #1915 */ RoundingMode arg0(node[0].getConst<RoundingMode>()); @@ -1110,9 +1099,6 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Unreachable() << "Unknown rounding mode in roundingModeBitBlast"; break; } -#else - value = BitVector(5U, 0U); -#endif return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(value)); } diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index b78ef24c7..77c1ef8f0 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -727,7 +727,6 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, } } -#ifdef CVC5_USE_SYMFPU /* Need to create some symfpu objects as the size of bit-vector * that is needed for this component is dependent on the encoding * used (i.e. whether subnormals are forcibly normalised or not). @@ -735,9 +734,6 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, * back-end but it should't make a difference. */ FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); uint32_t bw = FloatingPoint::getUnpackedExponentWidth(fps); -#else - uint32_t bw = 2; -#endif return nodeManager->mkBitVectorType(bw); } @@ -767,13 +763,9 @@ TypeNode FloatingPointComponentSignificand::computeType( } } -#ifdef CVC5_USE_SYMFPU /* As before we need to use some of sympfu. */ FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps); -#else - uint32_t bw = 1; -#endif return nodeManager->mkBitVectorType(bw); } diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index fe4ed4c22..778c842a6 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -75,6 +75,10 @@ const char* toString(InferenceId i) return "ARITH_NL_IAND_SUM_REFINE"; case InferenceId::ARITH_NL_IAND_BITWISE_REFINE: return "ARITH_NL_IAND_BITWISE_REFINE"; + case InferenceId::ARITH_NL_POW2_INIT_REFINE: + return "ARITH_NL_POW2_INIT_REFINE"; + case InferenceId::ARITH_NL_POW2_VALUE_REFINE: + return "ARITH_NL_POW2_VALUE_REFINE"; case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT"; case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: return "ARITH_NL_CAD_EXCLUDED_INTERVAL"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 169992f41..6a87776d6 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -126,6 +126,11 @@ enum class InferenceId ARITH_NL_IAND_SUM_REFINE, // bitwise refinements (IAndSolver::checkFullRefine) ARITH_NL_IAND_BITWISE_REFINE, + //-------------------- nonlinear pow2 solver + // initial refinements (Pow2Solver::checkInitialRefine) + ARITH_NL_POW2_INIT_REFINE, + // value refinements (Pow2Solver::checkFullRefine) + ARITH_NL_POW2_VALUE_REFINE, //-------------------- nonlinear cad solver // conflict / infeasible subset obtained from cad ARITH_NL_CAD_CONFLICT, diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 8ba43aa1a..d53b06151 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -44,10 +44,6 @@ LogicInfo::LogicInfo() { for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { - if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU()) - { - continue; - } enableTheory(id); } } diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 808db7aec..c6f38f298 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -941,8 +941,9 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n else if( n.getNumChildren()==0 ){ Node r = n; if( !n.isConst() ){ - if( !fm->hasTerm(n) ){ - r = getSomeDomainElement(fm, n.getType() ); + TypeNode tn = n.getType(); + if( !fm->hasTerm(n) && tn.isFirstClass() ){ + r = getSomeDomainElement(fm, tn ); } r = fm->getRepresentative( r ); } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 71f4028ec..0f82d8301 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/instantiate.h" #include "expr/node_algorithm.h" +#include "options/base_options.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 5b7bd1552..31e5240df 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/term_registry.h" +#include "options/base_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "theory/quantifiers/first_order_model.h" diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 6d1b9955a..efede77ba 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -95,6 +95,7 @@ bool TheorySep::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; esi.d_name = "theory::sep::ee"; + esi.d_notifyMerge = true; return true; } diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 4cca76057..439e9443d 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -60,6 +60,9 @@ bool TheorySets::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; esi.d_name = "theory::sets::ee"; + esi.d_notifyNewClass = true; + esi.d_notifyMerge = true; + esi.d_notifyDisequal = true; return true; } diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index 3d4a2d143..be1646403 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -364,6 +364,10 @@ bool RegExpEntail::isConstRegExp(TNode t) } } } + else if (ck == ITE) + { + return false; + } else if (cur.isVar()) { return false; diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index aac9e9313..8c5805b37 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -249,7 +249,8 @@ void TermRegistry::preRegisterTerm(TNode n) // Concatenation terms do not need to be considered here because // their arguments have string type and do not introduce any shared // terms. - if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT) + if (n.hasOperator() && ee->isFunctionKind(k) + && kindToTheoryId(k) == THEORY_STRINGS && k != STRING_CONCAT) { d_functionsTerms.push_back(n); } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f4daed85d..f0763e153 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -103,6 +103,9 @@ bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; esi.d_name = "theory::strings::ee"; + esi.d_notifyNewClass = true; + esi.d_notifyMerge = true; + esi.d_notifyDisequal = true; return true; } diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index d6ad4cd41..b9dc1ba42 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -330,12 +330,18 @@ bool Theory::isLegalElimination(TNode x, TNode val) { return false; } - if (!options::produceModels()) + if (!options::produceModels() && !d_logicInfo.isQuantified()) { - // don't care about the model, we are fine + // Don't care about the model and logic is not quantified, we can eliminate. return true; } - // if there is a model object + // If models are enabled, then it depends on whether the term contains any + // unevaluable operators like FORALL, SINE, etc. Having such operators makes + // model construction contain non-constant values for variables, which is + // not ideal from a user perspective. + // We also insist on this check since the term to eliminate should never + // contain quantifiers, or else variable shadowing issues may arise. + // there should be a model object TheoryModel* tm = d_valuation.getModel(); Assert(tm != nullptr); return tm->isLegalElimination(x, val); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 8eec7f911..3e902463c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -142,8 +142,22 @@ Node TheoryModel::getValue(TNode n) const Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl; //get value in model nn = getModelValue(nn); - if (nn.isNull()) return nn; - if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { + if (nn.isNull()) + { + return nn; + } + else if (nn.getKind() == kind::LAMBDA) + { + if (options::condenseFunctionValues()) + { + // normalize the body. Do not normalize the entire node, which + // involves array normalization. + NodeManager* nm = NodeManager::currentNM(); + nn = nm->mkNode(kind::LAMBDA, nn[0], Rewriter::rewrite(nn[1])); + } + } + else + { //normalize nn = Rewriter::rewrite(nn); } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 8885abe6b..338076e78 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -88,10 +88,6 @@ void EqualityEngine::init() { d_triggerDatabaseAllocatedSize = 100000; d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize); - //We can't notify during the initialization because it notifies - // QuantifiersEngine.AddTermToDatabase that try to access to the uf - // instantiator that currently doesn't exist. - ScopedBool sb(d_performNotify, false); addTermInternal(d_true); addTermInternal(d_false); @@ -111,7 +107,6 @@ EqualityEngine::EqualityEngine(context::Context* context, d_masterEqualityEngine(0), d_context(context), d_done(context, false), - d_performNotify(true), d_notify(s_notifyNone), d_applicationLookupsCount(context, 0), d_nodesCount(context, 0), @@ -141,7 +136,6 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, d_masterEqualityEngine(0), d_context(context), d_done(context, false), - d_performNotify(true), d_notify(notify), d_applicationLookupsCount(context, 0), d_nodesCount(context, 0), @@ -381,10 +375,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { { // Notify e.g. the theory that owns this equality engine that there is a // new equivalence class. - if (d_performNotify) - { - d_notify.eqNotifyNewClass(t); - } + d_notify.eqNotifyNewClass(t); if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags @@ -506,9 +497,7 @@ bool EqualityEngine::assertEquality(TNode eq, } // notify the theory - if (d_performNotify) { - d_notify.eqNotifyDisequal(eq[0], eq[1], reason); - } + d_notify.eqNotifyDisequal(eq[0], eq[1], reason); Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; @@ -608,7 +597,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Determine if we should notify the owner of this class of this merge. // The second part of this check is needed due to the internal implementation // of this class. It ensures that we are merging terms and not operators. - if (d_performNotify && class1Id == cc1.getFind() && class2Id == cc2.getFind()) + if (class1Id == cc1.getFind() && class2Id == cc2.getFind()) { doNotify = true; } @@ -797,11 +786,11 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = class1triggers.d_triggers[i1++]; // since they are both tagged notify of merge - if (d_performNotify) { - EqualityNodeId tag2id = class2triggers.d_triggers[i2++]; - if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { - return false; - } + EqualityNodeId tag2id = class2triggers.d_triggers[i2++]; + if (!d_notify.eqNotifyTriggerTermEquality( + tag1, d_nodes[tag1id], d_nodes[tag2id], true)) + { + return false; } // Next tags tag1 = TheoryIdSetUtil::setPop(tags1); @@ -1934,9 +1923,8 @@ void EqualityEngine::propagate() { d_assertedEqualities.push_back(Equality(null_id, null_id)); d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; // Notify - if (d_performNotify) { - d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], d_nodes[t2classId]); - } + d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], + d_nodes[t2classId]); // Empty the queue and exit continue; } @@ -1995,7 +1983,8 @@ void EqualityEngine::propagate() { } // Notify the triggers - if (d_performNotify && !d_done) { + if (!d_done) + { for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) { const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]]; if (triggerInfo.d_trigger.getKind() == kind::EQUAL) @@ -2217,12 +2206,16 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId]; if (triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag)) { // If the term already is in the equivalence class that a tagged representative, just notify - if (d_performNotify) { - EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag); - Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << "): already have this trigger in class with " << d_nodes[triggerId] << std::endl; - if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) { - d_done = true; - } + EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag); + Debug("equality::trigger") + << d_name << "::eq::addTriggerTerm(" << t << ", " << tag + << "): already have this trigger in class with " << d_nodes[triggerId] + << std::endl; + if (eqNodeId != triggerId + && !d_notify.eqNotifyTriggerTermEquality( + tag, t, d_nodes[triggerId], true)) + { + d_done = true; } } else { @@ -2602,10 +2595,10 @@ bool EqualityEngine::propagateTriggerTermDisequalities( // Store the propagation storePropagatedDisequality(currentTag, myRep, tagRep); // Notify - if (d_performNotify) { - if (!d_notify.eqNotifyTriggerTermEquality(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) { - d_done = true; - } + if (!d_notify.eqNotifyTriggerTermEquality( + currentTag, d_nodes[myRep], d_nodes[tagRep], false)) + { + d_done = true; } } } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 024774593..c0e7b3478 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -120,9 +120,6 @@ private: /** If we are done, we don't except any new assertions */ context::CDO<bool> d_done; - /** Whether to notify or not (temporarily disabled on equality checks) */ - bool d_performNotify; - /** The class to notify when a representative changes for a term */ EqualityEngineNotify& d_notify; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 36b05b145..f1adde143 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -73,6 +73,14 @@ bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; esi.d_name = d_instanceName + "theory::uf::ee"; + if (options::finiteModelFind() + && options::ufssMode() != options::UfssMode::NONE) + { + // need notifications about sorts + esi.d_notifyNewClass = true; + esi.d_notifyMerge = true; + esi.d_notifyDisequal = true; + } return true; } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 2938ddcca..71742dfce 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -13,9 +13,6 @@ # The build system configuration. ## -configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.h) -configure_file(floatingpoint_literal_symfpu_traits.h.in - floatingpoint_literal_symfpu_traits.h) configure_file(rational.h.in rational.h) configure_file(integer.h.in integer.h) configure_file(real_algebraic_number.h.in real_algebraic_number.h) diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index c2c3fe77b..dc3dce6b9 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -16,7 +16,6 @@ #include "base/check.h" -#ifdef CVC5_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" #include "symfpu/core/compare.h" @@ -31,11 +30,9 @@ #include "symfpu/core/sqrt.h" #include "symfpu/utils/numberOfRoundingModes.h" #include "symfpu/utils/properties.h" -#endif /* -------------------------------------------------------------------------- */ -#ifdef CVC5_USE_SYMFPU namespace symfpu { #define CVC5_LIT_ITE_DFN(T) \ @@ -57,7 +54,6 @@ CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::ubv); #undef CVC5_LIT_ITE_DFN } // namespace symfpu -#endif /* -------------------------------------------------------------------------- */ @@ -65,44 +61,30 @@ namespace cvc5 { uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size) { -#ifdef CVC5_USE_SYMFPU return SymFPUUnpackedFloatLiteral::exponentWidth(size); -#else - unimplemented(); - return 2; -#endif } uint32_t FloatingPointLiteral::getUnpackedSignificandWidth( FloatingPointSize& size) { -#ifdef CVC5_USE_SYMFPU return SymFPUUnpackedFloatLiteral::significandWidth(size); -#else - unimplemented(); - return 2; -#endif } FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size, uint32_t sig_size, const BitVector& bv) : d_fp_size(exp_size, sig_size) -#ifdef CVC5_USE_SYMFPU , d_symuf(symfpu::unpack<symfpuLiteral::traits>( symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv)) -#endif { } FloatingPointLiteral::FloatingPointLiteral( const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size)) -#endif { Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN); } @@ -112,12 +94,10 @@ FloatingPointLiteral::FloatingPointLiteral( FloatingPointLiteral::SpecialConstKind kind, bool sign) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF ? SymFPUUnpackedFloatLiteral::makeInf(size, sign) : SymFPUUnpackedFloatLiteral::makeZero(size, sign)) -#endif { Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF || kind == FloatingPointLiteral::SpecialConstKind::FPZERO); @@ -126,10 +106,8 @@ FloatingPointLiteral::FloatingPointLiteral( FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv)) -#endif { } @@ -138,7 +116,6 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv, bool signedBV) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>( symfpuLiteral::Cvc5FPSize(size), @@ -148,97 +125,61 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, symfpuLiteral::Cvc5FPSize(size), symfpuLiteral::Cvc5RM(rm), symfpuLiteral::Cvc5UnsignedBitVector(bv))) -#endif { } BitVector FloatingPointLiteral::pack(void) const { -#ifdef CVC5_USE_SYMFPU BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - BitVector bv(4u, 0u); -#endif return bv; } FloatingPointLiteral FloatingPointLiteral::absolute(void) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::negate(void) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::add( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::add<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf, true)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::sub( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::add<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf, false)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::mult( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::multiply<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::div( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::divide<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::fma( @@ -246,276 +187,150 @@ FloatingPointLiteral FloatingPointLiteral::fma( const FloatingPointLiteral& arg1, const FloatingPointLiteral& arg2) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg1.d_fp_size); Assert(d_fp_size == arg2.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::fma<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::rem( const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::remainder<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::maxTotal( const FloatingPointLiteral& arg, bool zeroCaseLeft) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::max<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::minTotal( const FloatingPointLiteral& arg, bool zeroCaseLeft) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::min<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft)); -#else - unimplemented(); - return *this; -#endif } bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const { -#ifdef CVC5_USE_SYMFPU return ((d_fp_size == fp.d_fp_size) && symfpu::smtlibEqual<symfpuLiteral::traits>( d_fp_size, d_symuf, fp.d_symuf)); -#else - unimplemented(); - return ((d_fp_size == fp.d_fp_size)); -#endif } bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThanOrEqual<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThan<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf); -#else - unimplemented(); - return false; -#endif } BitVector FloatingPointLiteral::getExponent() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.exponent; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return BitVector(); -#endif } BitVector FloatingPointLiteral::getSignificand() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.significand; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return BitVector(); -#endif } bool FloatingPointLiteral::getSign() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.sign; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return false; -#endif } bool FloatingPointLiteral::isNormal(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isSubnormal(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isZero(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isInfinite(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isNaN(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isNegative(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isPositive(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } FloatingPointLiteral FloatingPointLiteral::convert( const FloatingPointSize& target, const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( target, symfpu::convertFloatToFloat<symfpuLiteral::traits>( d_fp_size, target, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const { -#ifdef CVC5_USE_SYMFPU return symfpu::convertFloatToSBV<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, width, undefinedCase); -#else - unimplemented(); - return undefinedCase; -#endif } BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const { -#ifdef CVC5_USE_SYMFPU return symfpu::convertFloatToUBV<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, width, undefinedCase); -#else - unimplemented(); - return undefinedCase; -#endif } -#ifndef CVC5_USE_SYMFPU -void FloatingPointLiteral::unimplemented(void) -{ - Unimplemented() << "no concrete implementation of FloatingPointLiteral"; -} - -size_t FloatingPointLiteral::hash(void) const -{ - unimplemented(); - return 23; -} -#endif - } // namespace cvc5 diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h index 54827a308..5b2b0f7c8 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h @@ -20,20 +20,16 @@ #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H #include "util/bitvector.h" -#include "util/floatingpoint_size.h" #include "util/floatingpoint_literal_symfpu_traits.h" +#include "util/floatingpoint_size.h" #include "util/roundingmode.h" /* -------------------------------------------------------------------------- */ namespace cvc5 { -// clang-format off -#if @CVC5_USE_SYMFPU@ -// clang-format on using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>; -#endif class FloatingPointLiteral { @@ -65,13 +61,6 @@ class FloatingPointLiteral */ static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size); -// clang-format off -#if !@CVC5_USE_SYMFPU@ - // clang-format on - /** Catch-all for unimplemented functions. */ - static void unimplemented(void); -#endif - /** Constructors. */ /** Create a FP literal from its IEEE bit-vector representation. */ @@ -197,18 +186,10 @@ class FloatingPointLiteral BitVector convertToUBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const; -// clang-format off -#if @CVC5_USE_SYMFPU@ - // clang-format on /** Return wrapped floating-point literal. */ const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; } -#else - /** Dummy hash function. */ - size_t hash(void) const; -#endif private: - /** * Create a FP literal from unpacked representation. * @@ -223,34 +204,19 @@ class FloatingPointLiteral const bool sign, const BitVector& exp, const BitVector& sig) - : d_fp_size(size) -// clang-format off -#if @CVC5_USE_SYMFPU@ - // clang-format on - , - d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) -#endif + : d_fp_size(size), d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) { } -// clang-format off -#if @CVC5_USE_SYMFPU@ - // clang-format on - /** Create a FP literal from a symFPU unpacked float. */ FloatingPointLiteral(const FloatingPointSize& size, SymFPUUnpackedFloatLiteral symuf) : d_fp_size(size), d_symuf(symuf){}; -#endif /** The floating-point size of this floating-point literal. */ FloatingPointSize d_fp_size; -// clang-format off -#if @CVC5_USE_SYMFPU@ - // clang-format on /** The actual floating-point value, a SymFPU unpackedFloat. */ SymFPUUnpackedFloatLiteral d_symuf; -#endif }; /* -------------------------------------------------------------------------- */ diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp index 071b69912..0f46708b0 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.cpp +++ b/src/util/floatingpoint_literal_symfpu_traits.cpp @@ -13,8 +13,6 @@ * SymFPU glue code for floating-point values. */ -#if CVC5_USE_SYMFPU - #include "util/floatingpoint_literal_symfpu_traits.h" #include "base/check.h" @@ -413,4 +411,3 @@ void traits::invariant(const traits::prop& p) } } // namespace symfpuLiteral } // namespace cvc5 -#endif diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h index 76d2f47e2..bc5caaf88 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.h.in +++ b/src/util/floatingpoint_literal_symfpu_traits.h @@ -25,16 +25,12 @@ #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H -// clang-format off -#if @CVC5_USE_SYMFPU@ -// clang-format on +#include <symfpu/core/unpackedFloat.h> #include "util/bitvector.h" #include "util/floatingpoint_size.h" #include "util/roundingmode.h" -#include <symfpu/core/unpackedFloat.h> - /* -------------------------------------------------------------------------- */ namespace cvc5 { @@ -258,7 +254,6 @@ class wrappedBitVector : public BitVector Cvc5BitWidth lower) const; }; } // namespace symfpuLiteral -} +} // namespace cvc5 #endif -#endif diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index f0cc78789..c4a94dfa2 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -22,9 +22,9 @@ #include "base/check.h" #include "base/listener.h" #include "base/output.h" +#include "options/base_options.h" #include "options/option_exception.h" #include "options/options.h" -#include "options/resource_manager_options.h" #include "util/statistics_registry.h" using namespace std; @@ -164,7 +164,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, d_infidWeights.fill(1); d_resourceWeights.fill(1); - for (const auto& opt : d_options.resman.resourceWeightHolder) + for (const auto& opt : d_options.base.resourceWeightHolder) { std::string name; uint64_t weight; @@ -189,9 +189,9 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; } uint64_t ResourceManager::getResourceRemaining() const { - if (d_options.resman.cumulativeResourceLimit <= d_cumulativeResourceUsed) + if (d_options.base.cumulativeResourceLimit <= d_cumulativeResourceUsed) return 0; - return d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed; + return d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed; } void ResourceManager::spendResource(uint64_t amount) @@ -237,21 +237,21 @@ void ResourceManager::spendResource(theory::InferenceId iid) void ResourceManager::beginCall() { - d_perCallTimer.set(d_options.resman.perCallMillisecondLimit); + d_perCallTimer.set(d_options.base.perCallMillisecondLimit); d_thisCallResourceUsed = 0; - if (d_options.resman.cumulativeResourceLimit > 0) + if (d_options.base.cumulativeResourceLimit > 0) { // Compute remaining cumulative resource budget d_thisCallResourceBudget = - d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed; + d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed; } - if (d_options.resman.perCallResourceLimit > 0) + if (d_options.base.perCallResourceLimit > 0) { // Check if per-call resource budget is even smaller - if (d_options.resman.perCallResourceLimit < d_thisCallResourceBudget) + if (d_options.base.perCallResourceLimit < d_thisCallResourceBudget) { - d_thisCallResourceBudget = d_options.resman.perCallResourceLimit; + d_thisCallResourceBudget = d_options.base.perCallResourceLimit; } } } @@ -265,25 +265,25 @@ void ResourceManager::endCall() bool ResourceManager::limitOn() const { - return (d_options.resman.cumulativeResourceLimit > 0) - || (d_options.resman.perCallMillisecondLimit > 0) - || (d_options.resman.perCallResourceLimit > 0); + return (d_options.base.cumulativeResourceLimit > 0) + || (d_options.base.perCallMillisecondLimit > 0) + || (d_options.base.perCallResourceLimit > 0); } bool ResourceManager::outOfResources() const { - if (d_options.resman.perCallResourceLimit > 0) + if (d_options.base.perCallResourceLimit > 0) { // Check if per-call resources are exhausted - if (d_thisCallResourceUsed >= d_options.resman.perCallResourceLimit) + if (d_thisCallResourceUsed >= d_options.base.perCallResourceLimit) { return true; } } - if (d_options.resman.cumulativeResourceLimit > 0) + if (d_options.base.cumulativeResourceLimit > 0) { // Check if cumulative resources are exhausted - if (d_cumulativeResourceUsed >= d_options.resman.cumulativeResourceLimit) + if (d_cumulativeResourceUsed >= d_options.base.cumulativeResourceLimit) { return true; } @@ -293,7 +293,7 @@ bool ResourceManager::outOfResources() const bool ResourceManager::outOfTime() const { - if (d_options.resman.perCallMillisecondLimit == 0) return false; + if (d_options.base.perCallMillisecondLimit == 0) return false; return d_perCallTimer.expired(); } |