diff options
Diffstat (limited to 'src/theory')
41 files changed, 499 insertions, 141 deletions
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; } |