diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-27 08:14:19 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-27 08:14:19 -0700 |
commit | 8f8d2193277d75c7b3631af235b0a23de7f04926 (patch) | |
tree | 24f7b6b2c1e28b988f4ddd61f9761777caebf487 | |
parent | 0b82388e10cbb2ae7fc2f2c81ee643c5dd6f2605 (diff) | |
parent | 9f9f8d29c9428289492e421fc1c464a51a06977e (diff) |
Merge branch 'master' into rmCoverityrmCoverity
38 files changed, 1281 insertions, 936 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 3b8a12fa5..3681280ec 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -65,6 +65,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/apply_substs.h \ preprocessing/passes/apply_to_const.cpp \ preprocessing/passes/apply_to_const.h \ + preprocessing/passes/bool_to_bv.cpp \ + preprocessing/passes/bool_to_bv.h \ preprocessing/passes/bv_abstraction.cpp \ preprocessing/passes/bv_abstraction.h \ preprocessing/passes/bv_ackermann.cpp \ @@ -75,6 +77,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bv_gauss.h \ preprocessing/passes/bv_intro_pow2.cpp \ preprocessing/passes/bv_intro_pow2.h \ + preprocessing/passes/bv_to_bool.cpp \ + preprocessing/passes/bv_to_bool.h \ preprocessing/passes/extended_rewriter_pass.cpp \ preprocessing/passes/extended_rewriter_pass.h \ preprocessing/passes/global_negate.cpp \ @@ -85,14 +89,14 @@ libcvc4_la_SOURCES = \ preprocessing/passes/ite_removal.h \ preprocessing/passes/ite_simp.cpp \ preprocessing/passes/ite_simp.h \ + preprocessing/passes/nl_ext_purify.cpp \ + preprocessing/passes/nl_ext_purify.h \ preprocessing/passes/pseudo_boolean_processor.cpp \ preprocessing/passes/pseudo_boolean_processor.h \ - preprocessing/passes/bool_to_bv.cpp \ - preprocessing/passes/bool_to_bv.h \ - preprocessing/passes/bv_to_bool.cpp \ - preprocessing/passes/bv_to_bool.h \ preprocessing/passes/quantifiers_preprocess.cpp \ preprocessing/passes/quantifiers_preprocess.h \ + preprocessing/passes/quantifier_macros.cpp \ + preprocessing/passes/quantifier_macros.h \ preprocessing/passes/real_to_int.cpp \ preprocessing/passes/real_to_int.h \ preprocessing/passes/rewrite.cpp \ @@ -111,6 +115,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/symmetry_detect.h \ preprocessing/passes/synth_rew_rules.cpp \ preprocessing/passes/synth_rew_rules.h \ + preprocessing/passes/unconstrained_simplifier.cpp \ + preprocessing/passes/unconstrained_simplifier.h \ preprocessing/preprocessing_pass.cpp \ preprocessing/preprocessing_pass.h \ preprocessing/preprocessing_pass_context.cpp \ @@ -240,8 +246,6 @@ libcvc4_la_SOURCES = \ theory/type_enumerator.h \ theory/type_set.cpp \ theory/type_set.h \ - theory/unconstrained_simplifier.cpp \ - theory/unconstrained_simplifier.h \ theory/valuation.cpp \ theory/valuation.h \ theory/arith/approx_simplex.cpp \ @@ -480,8 +484,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/lazy_trie.h \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/local_theory_ext.h \ - theory/quantifiers/macros.cpp \ - theory/quantifiers/macros.h \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/quant_conflict_find.h \ theory/quantifiers/quant_epr.cpp \ diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp new file mode 100644 index 000000000..afb092571 --- /dev/null +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -0,0 +1,130 @@ +/********************* */ +/*! \file nl_ext_purify.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief The NlExtPurify preprocessing pass + ** + ** Purifies non-linear terms + **/ + +#include "preprocessing/passes/nl_ext_purify.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +Node NlExtPurify::purifyNlTerms(TNode n, + NodeMap& cache, + NodeMap& bcache, + std::vector<Node>& var_eq, + bool beneathMult) +{ + if (beneathMult) + { + NodeMap::iterator find = bcache.find(n); + if (find != bcache.end()) + { + return (*find).second; + } + } + else + { + NodeMap::iterator find = cache.find(n); + if (find != cache.end()) + { + return (*find).second; + } + } + Node ret = n; + if (n.getNumChildren() > 0) + { + if (beneathMult + && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) + { + // don't do it if it rewrites to a constant + Node nr = Rewriter::rewrite(n); + if (nr.isConst()) + { + // return the rewritten constant + ret = nr; + } + else + { + // new variable + ret = NodeManager::currentNM()->mkSkolem( + "__purifyNl_var", + n.getType(), + "Variable introduced in purifyNl pass"); + Node np = purifyNlTerms(n, cache, bcache, var_eq, false); + var_eq.push_back(np.eqNode(ret)); + Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np + << std::endl; + } + } + else + { + bool beneathMultNew = beneathMult || n.getKind() == kind::MULT; + bool childChanged = false; + std::vector<Node> children; + for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i) + { + Node nc = purifyNlTerms(n[i], cache, bcache, var_eq, beneathMultNew); + childChanged = childChanged || nc != n[i]; + children.push_back(nc); + } + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(n.getKind(), children); + } + } + } + if (beneathMult) + { + bcache[n] = ret; + } + else + { + cache[n] = ret; + } + return ret; +} + +NlExtPurify::NlExtPurify(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "nl-ext-purify"){}; + +PreprocessingPassResult NlExtPurify::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + unordered_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> bcache; + std::vector<Node> var_eq; + unsigned size = assertionsToPreprocess->size(); + for (unsigned i = 0; i < size; ++i) + { + Node a = (*assertionsToPreprocess)[i]; + assertionsToPreprocess->replace(i, purifyNlTerms(a, cache, bcache, var_eq)); + Trace("nl-ext-purify") << "Purify : " << a << " -> " + << (*assertionsToPreprocess)[i] << "\n"; + } + if (!var_eq.empty()) + { + unsigned lastIndex = size - 1; + var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]); + assertionsToPreprocess->replace( + lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq)); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h new file mode 100644 index 000000000..8d28b0742 --- /dev/null +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file nl_ext_purify.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief The NlExtPurify preprocessing pass + ** + ** Purifies non-linear terms by replacing sums under multiplications by fresh + ** variables + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H +#define __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H + +#include <unordered_map> +#include <vector> + +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>; + +class NlExtPurify : public PreprocessingPass +{ + public: + NlExtPurify(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + Node purifyNlTerms(TNode n, + NodeMap& cache, + NodeMap& bcache, + std::vector<Node>& var_eq, + bool beneathMult = false); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ diff --git a/src/theory/quantifiers/macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index d88f8eec9..e3bc02309 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file macros.cpp +/*! \file quantifier_macros.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Kshitij Bansal @@ -14,7 +14,7 @@ ** This class implements quantifiers macro definitions. **/ -#include "theory/quantifiers/macros.h" +#include "preprocessing/passes/quantifier_macros.h" #include <vector> @@ -27,19 +27,48 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" -using namespace CVC4; using namespace std; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; +namespace CVC4 { +namespace preprocessing { +namespace passes { -QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){ +QuantifierMacros::QuantifierMacros(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "quantifier-macros"), + d_ground_macros(false) +{ +} + +PreprocessingPassResult QuantifierMacros::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + bool success; + do + { + success = simplify(assertionsToPreprocess->ref(), true); + } while (success); + finalizeDefinitions(); + clearMaps(); + return PreprocessingPassResult::NO_CONFLICT; +} + +void QuantifierMacros::clearMaps() +{ + d_macro_basis.clear(); + d_macro_defs.clear(); + d_macro_defs_new.clear(); + d_macro_def_contains.clear(); + d_simplify_cache.clear(); + d_quant_macros.clear(); d_ground_macros = false; } - + bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; for( unsigned r=0; r<rmax; r++ ){ @@ -72,14 +101,14 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite //for now, it is dependent upon all assertions involving macros, this is an over-approximation. //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula, // which is expensive. - PROOF( - ProofManager::currentPM()->addDependence(curr, assertions[i]); - for( unsigned j=0; j<macro_assertions.size(); j++ ){ - if( macro_assertions[j]!=assertions[i] ){ - ProofManager::currentPM()->addDependence(curr,macro_assertions[j]); - } - } - ); + PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]); + for (unsigned j = 0; j < macro_assertions.size(); j++) { + if (macro_assertions[j] != assertions[i]) + { + ProofManager::currentPM()->addDependence( + curr, macro_assertions[j]); + } + }); assertions[i] = curr; retVal = true; } @@ -154,7 +183,10 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ } bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { - Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f); + Node icn = d_preprocContext->getTheoryEngine() + ->getQuantifiersEngine() + ->getTermUtil() + ->substituteBoundVariablesToInstConstants(n, f); Trace("macros-debug2") << "Get free variables in " << icn << std::endl; std::vector< Node > var; quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var); @@ -512,3 +544,7 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { } } } + +} // passes +} // preprocessing +} // CVC4 diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h new file mode 100644 index 000000000..092a62942 --- /dev/null +++ b/src/preprocessing/passes/quantifier_macros.h @@ -0,0 +1,89 @@ +/********************* */ +/*! \file quantifier_macros.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief Pre-process step for detecting quantifier macro definitions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H + +#include <map> +#include <string> +#include <vector> +#include "expr/node.h" +#include "expr/type_node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class QuantifierMacros : public PreprocessingPass +{ + public: + QuantifierMacros(PreprocessingPassContext* preprocContext); + ~QuantifierMacros() {} + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + bool processAssertion(Node n); + bool isBoundVarApplyUf(Node n); + bool process(Node n, bool pol, std::vector<Node>& args, Node f); + bool containsBadOp(Node n, + Node op, + std::vector<Node>& opc, + std::map<Node, bool>& visited); + bool isMacroLiteral(Node n, bool pol); + bool isGroundUfTerm(Node f, Node n); + void getMacroCandidates(Node n, + std::vector<Node>& candidates, + std::map<Node, bool>& visited); + Node solveInEquality(Node n, Node lit); + bool getFreeVariables(Node n, + std::vector<Node>& v_quant, + std::vector<Node>& vars, + bool retOnly, + std::map<Node, bool>& visited); + bool getSubstitution(std::vector<Node>& v_quant, + std::map<Node, Node>& solved, + std::vector<Node>& vars, + std::vector<Node>& subs, + bool reqComplete); + void addMacro(Node op, Node n, std::vector<Node>& opc); + void debugMacroDefinition(Node oo, Node n); + bool simplify(std::vector<Node>& assertions, bool doRewrite = false); + Node simplify(Node n); + void finalizeDefinitions(); + void clearMaps(); + + // map from operators to macro basis terms + std::map<Node, std::vector<Node> > d_macro_basis; + // map from operators to macro definition + std::map<Node, Node> d_macro_defs; + std::map<Node, Node> d_macro_defs_new; + // operators to macro ops that contain them + std::map<Node, std::vector<Node> > d_macro_def_contains; + // simplify caches + std::map<Node, Node> d_simplify_cache; + std::map<Node, bool> d_quant_macros; + bool d_ground_macros; +}; + +} // passes +} // preprocessing +} // CVC4 + +#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ diff --git a/src/theory/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 41529760b..6bb46f3f2 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -11,44 +11,46 @@ ** ** \brief Simplifications based on unconstrained variables ** - ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions - ** by variables. Based on Roberto Bruttomesso's PhD thesis. + ** This module implements a preprocessing phase which replaces certain + ** "unconstrained" expressions by variables. Based on Roberto + ** Bruttomesso's PhD thesis. **/ +#include "preprocessing/passes/unconstrained_simplifier.h" -#include "theory/unconstrained_simplifier.h" - -#include "theory/rewriter.h" -#include "theory/logic_info.h" #include "smt/smt_statistics_registry.h" +#include "theory/logic_info.h" +#include "theory/rewriter.h" -using namespace std; -using namespace CVC4; -using namespace theory; +namespace CVC4 { +namespace preprocessing { +namespace passes { +using namespace CVC4::theory; -UnconstrainedSimplifier::UnconstrainedSimplifier(context::Context* context, - const LogicInfo& logicInfo) - : d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), - d_context(context), d_substitutions(context), d_logicInfo(logicInfo) +UnconstrainedSimplifier::UnconstrainedSimplifier( + PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "unconstrained-simplifier"), + d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), + d_context(preprocContext->getDecisionContext()), + d_substitutions(preprocContext->getDecisionContext()), + d_logicInfo(preprocContext->getLogicInfo()) { smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim); } - UnconstrainedSimplifier::~UnconstrainedSimplifier() { smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim); } - -struct unc_preprocess_stack_element { +struct unc_preprocess_stack_element +{ TNode node; TNode parent; unc_preprocess_stack_element(TNode n) : node(n) {} unc_preprocess_stack_element(TNode n, TNode p) : node(n), parent(p) {} -};/* struct unc_preprocess_stack_element */ - +}; /* struct unc_preprocess_stack_element */ void UnconstrainedSimplifier::visitAll(TNode assertion) { @@ -64,10 +66,13 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) toVisit.pop_back(); TNodeCountMap::iterator find = d_visited.find(current); - if (find != d_visited.end()) { - if (find->second == 1) { + if (find != d_visited.end()) + { + if (find->second == 1) + { d_visitedOnce.erase(current); - if (current.isVar()) { + if (current.isVar()) + { d_unconstrained.erase(current); } } @@ -78,14 +83,18 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) d_visited[current] = 1; d_visitedOnce[current] = parent; - if (current.getNumChildren() == 0) { - if (current.getKind()==kind::VARIABLE || current.getKind()==kind::SKOLEM) { + if (current.getNumChildren() == 0) + { + if (current.getKind() == kind::VARIABLE + || current.getKind() == kind::SKOLEM) + { d_unconstrained.insert(current); } } - else { - for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { - TNode childNode = *child_it; + else + { + for (TNode childNode : current) + { toVisit.push_back(unc_preprocess_stack_element(childNode, current)); } } @@ -94,18 +103,19 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) { - Node n = NodeManager::currentNM()->mkSkolem("unconstrained", t, "a new var introduced because of unconstrained variable " + var.toString()); + Node n = NodeManager::currentNM()->mkSkolem( + "unconstrained", + t, + "a new var introduced because of unconstrained variable " + + var.toString()); return n; } - void UnconstrainedSimplifier::processUnconstrained() { - TNodeSet::iterator it = d_unconstrained.begin(), iend = d_unconstrained.end(); - vector<TNode> workList; - for ( ; it != iend; ++it) { - workList.push_back(*it); - } + NodeManager* nm = NodeManager::currentNM(); + + vector<TNode> workList(d_unconstrained.begin(), d_unconstrained.end()); Node currentSub; TNode parent; bool swap; @@ -116,65 +126,94 @@ void UnconstrainedSimplifier::processUnconstrained() TNode current = workList.back(); workList.pop_back(); - for (;;) { + for (;;) + { Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); parent = d_visitedOnce[current]; - if (!parent.isNull()) { + if (!parent.isNull()) + { swap = isSigned = strict = false; bool checkParent = false; - switch (parent.getKind()) { - - // If-then-else operator - any two unconstrained children makes the parent unconstrained - case kind::ITE: { - Assert(parent[0] == current || parent[1] == current || parent[2] == current); - bool uCond = parent[0] == current || d_unconstrained.find(parent[0]) != d_unconstrained.end(); - bool uThen = parent[1] == current || d_unconstrained.find(parent[1]) != d_unconstrained.end(); - bool uElse = parent[2] == current || d_unconstrained.find(parent[2]) != d_unconstrained.end(); - if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse)) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + switch (parent.getKind()) + { + // If-then-else operator - any two unconstrained children makes the + // parent unconstrained + case kind::ITE: + { + Assert(parent[0] == current || parent[1] == current + || parent[2] == current); + bool uCond = + parent[0] == current + || d_unconstrained.find(parent[0]) != d_unconstrained.end(); + bool uThen = + parent[1] == current + || d_unconstrained.find(parent[1]) != d_unconstrained.end(); + bool uElse = + parent[2] == current + || d_unconstrained.find(parent[2]) != d_unconstrained.end(); + if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse)) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (uThen) { - if (parent[1] != current) { - if (parent[1].isVar()) { + if (uThen) + { + if (parent[1] != current) + { + if (parent[1].isVar()) + { currentSub = parent[1]; } - else { + else + { Assert(d_substitutions.hasSubstitution(parent[1])); currentSub = d_substitutions.apply(parent[1]); } } - else if (currentSub.isNull()) { + else if (currentSub.isNull()) + { currentSub = current; } } - else if (parent[2] != current) { - if (parent[2].isVar()) { + else if (parent[2] != current) + { + if (parent[2].isVar()) + { currentSub = parent[2]; } - else { + else + { Assert(d_substitutions.hasSubstitution(parent[2])); currentSub = d_substitutions.apply(parent[2]); } } - else if (currentSub.isNull()) { + else if (currentSub.isNull()) + { currentSub = current; } current = parent; } - else { + else + { currentSub = Node(); } } - else if (uCond) { + else if (uCond) + { Cardinality card = parent.getType().getCardinality(); - if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) { - // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result - // is unconstrained + if (card.isFinite() && !card.isLargeFinite() + && card.getFiniteCardinality() == 2) + { + // Special case: condition is unconstrained, then and else are + // different, and total cardinality of the type is 2, then the + // result is unconstrained Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); - if (test == NodeManager::currentNM()->mkConst<bool>(false)) { + if (test == nm->mkConst<bool>(false)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); @@ -185,24 +224,30 @@ void UnconstrainedSimplifier::processUnconstrained() break; } - // Comparisons that return a different type - assuming domains are larger than 1, any - // unconstrained child makes parent unconstrained as well + // Comparisons that return a different type - assuming domains are + // larger than 1, any unconstrained child makes parent unconstrained as + // well case kind::EQUAL: - if (parent[0].getType() != parent[1].getType()) { + if (parent[0].getType() != parent[1].getType()) + { TNode other = (parent[0] == current) ? parent[1] : parent[0]; - if (current.getType().isSubtypeOf(other.getType())) { + if (current.getType().isSubtypeOf(other.getType())) + { break; } } - if( parent[0].getType().isDatatype() ){ + if (parent[0].getType().isDatatype()) + { TypeNode tn = parent[0].getType(); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isRecursiveSingleton( tn.toType() ) ){ - //domain size may be 1 + if (dt.isRecursiveSingleton(tn.toType())) + { + // domain size may be 1 break; } } - if( parent[0].getType().isBoolean() ){ + if (parent[0].getType().isBoolean()) + { checkParent = true; break; } @@ -212,18 +257,21 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::GT: case kind::GEQ: { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - Assert(parent[0] != parent[1] && - (parent[0] == current || parent[1] == current)); - if (currentSub.isNull()) { + Assert(parent[0] != parent[1] + && (parent[0] == current || parent[1] == current)); + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; } - else { + else + { currentSub = Node(); } break; @@ -236,24 +284,28 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::UMINUS: ++d_numUnconstrainedElim; Assert(parent[0] == current); - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } current = parent; break; - // Unary operators that propagate unconstrainedness and return a different type + // Unary operators that propagate unconstrainedness and return a + // different type case kind::BITVECTOR_EXTRACT: ++d_numUnconstrainedElim; Assert(parent[0] == current); - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; break; - // Operators returning same type requiring all children to be unconstrained + // Operators returning same type requiring all children to be + // unconstrained case kind::AND: case kind::OR: case kind::IMPLIES: @@ -263,13 +315,16 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_NOR: { bool allUnconstrained = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { + for (TNode child : parent) + { + if (d_unconstrained.find(child) == d_unconstrained.end()) + { allUnconstrained = false; break; } } - if (allUnconstrained) { + if (allUnconstrained) + { checkParent = true; } } @@ -283,135 +338,177 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_UREM_TOTAL: case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: - case kind::BITVECTOR_SMOD: { + case kind::BITVECTOR_SMOD: + { bool allUnconstrained = true; bool allDifferent = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { + for (TNode::iterator child_it = parent.begin(); + child_it != parent.end(); + ++child_it) + { + if (d_unconstrained.find(*child_it) == d_unconstrained.end()) + { allUnconstrained = false; break; } - for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) { - if (*child_it == *child_it2) { + for (TNode::iterator child_it2 = child_it + 1; + child_it2 != parent.end(); + ++child_it2) + { + if (*child_it == *child_it2) + { allDifferent = false; break; } } } - if (allUnconstrained && allDifferent) { + if (allUnconstrained && allDifferent) + { checkParent = true; } break; } - // Requires all children to be unconstrained and different, and returns a different type + // Requires all children to be unconstrained and different, and returns + // a different type case kind::BITVECTOR_CONCAT: { bool allUnconstrained = true; bool allDifferent = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { + for (TNode::iterator child_it = parent.begin(); + child_it != parent.end(); + ++child_it) + { + if (d_unconstrained.find(*child_it) == d_unconstrained.end()) + { allUnconstrained = false; break; } - for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) { - if (*child_it == *child_it2) { + for (TNode::iterator child_it2 = child_it + 1; + child_it2 != parent.end(); + ++child_it2) + { + if (*child_it == *child_it2) + { allDifferent = false; break; } } } - if (allUnconstrained && allDifferent) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (allUnconstrained && allDifferent) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; } - else { + else + { currentSub = Node(); } } } break; - // N-ary operators returning same type requiring at least one child to be unconstrained + // N-ary operators returning same type requiring at least one child to + // be unconstrained case kind::PLUS: case kind::MINUS: - if (current.getType().isInteger() && - !parent.getType().isInteger()) { + if (current.getType().isInteger() && !parent.getType().isInteger()) + { break; } case kind::XOR: case kind::BITVECTOR_XOR: case kind::BITVECTOR_XNOR: case kind::BITVECTOR_PLUS: - case kind::BITVECTOR_SUB: - checkParent = true; - break; + case kind::BITVECTOR_SUB: checkParent = true; break; - // Multiplication/division: must be non-integer and other operand must be non-zero - case kind::MULT: { + // Multiplication/division: must be non-integer and other operand must + // be non-zero + case kind::MULT: case kind::DIVISION: + { Assert(parent.getNumChildren() == 2); TNode other; - if (parent[0] == current) { + if (parent[0] == current) + { other = parent[1]; } - else { + else + { Assert(parent[1] == current); other = parent[0]; } - if (d_unconstrained.find(other) != d_unconstrained.end()) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - if (current.getType().isInteger() && other.getType().isInteger()) { - Assert(parent.getKind() == kind::DIVISION || parent.getType().isInteger()); - if (parent.getKind() == kind::DIVISION) { + if (d_unconstrained.find(other) != d_unconstrained.end()) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + if (current.getType().isInteger() && other.getType().isInteger()) + { + Assert(parent.getKind() == kind::DIVISION + || parent.getType().isInteger()); + if (parent.getKind() == kind::DIVISION) + { break; } } ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } current = parent; } - else { + else + { currentSub = Node(); } } - else { - // if only the denominator of a division is unconstrained, can't set it to 0 so the result is not unconstrained - if (parent.getKind() == kind::DIVISION && current == parent[1]) { + else + { + // if only the denominator of a division is unconstrained, can't + // set it to 0 so the result is not unconstrained + if (parent.getKind() == kind::DIVISION && current == parent[1]) + { break; } - NodeManager* nm = NodeManager::currentNM(); - // if we are an integer, the only way we are unconstrained is if we are a MULT by -1 - if (current.getType().isInteger()) { + // if we are an integer, the only way we are unconstrained is if + // we are a MULT by -1 + if (current.getType().isInteger()) + { // div/mult by 1 should have been simplified Assert(other != nm->mkConst<Rational>(1)); - if (other == nm->mkConst<Rational>(-1)) { - // div by -1 should have been simplified + // div by -1 should have been simplified + if (other != nm->mkConst<Rational>(-1)) + { + break; + } + else + { Assert(parent.getKind() == kind::MULT); Assert(parent.getType().isInteger()); } - else { - break; - } } - else { - // TODO: could build ITE here + else + { + // TODO(#2377): could build ITE here Node test = other.eqNode(nm->mkConst<Rational>(0)); - if (Rewriter::rewrite(test) != nm->mkConst<bool>(false)) { + if (Rewriter::rewrite(test) != nm->mkConst<bool>(false)) + { break; } } ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } current = parent; @@ -425,97 +522,120 @@ void UnconstrainedSimplifier::processUnconstrained() { bool found = false; bool done = false; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if ((*child_it) == current) { - if (found) { + + for (TNode child : parent) + { + if (child == current) + { + if (found) + { done = true; break; } found = true; continue; } - else if (d_unconstrained.find(*child_it) != d_unconstrained.end()) { - continue; - } - else { - NodeManager* nm = NodeManager::currentNM(); - Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0)); + else if (d_unconstrained.find(child) == d_unconstrained.end()) + { + Node extractOp = + nm->mkConst<BitVectorExtract>(BitVectorExtract(0, 0)); vector<Node> children; - children.push_back(*child_it); + children.push_back(child); Node test = nm->mkNode(extractOp, children); - BitVector one(1,unsigned(1)); + BitVector one(1, unsigned(1)); test = test.eqNode(nm->mkConst<BitVector>(one)); - if (Rewriter::rewrite(test) != nm->mkConst<bool>(true)) { + if (Rewriter::rewrite(test) != nm->mkConst<bool>(true)) + { done = true; break; } } } - if (done) { + if (done) + { break; } checkParent = true; break; } - // Uninterpreted function - if domain is infinite, no quantifiers are used, and any child is unconstrained, result is unconstrained + // Uninterpreted function - if domain is infinite, no quantifiers are + // used, and any child is unconstrained, result is unconstrained case kind::APPLY_UF: - if (d_logicInfo.isQuantified() || !current.getType().getCardinality().isInfinite()) { + if (d_logicInfo.isQuantified() + || !current.getType().getCardinality().isInfinite()) + { break; } - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } - if (parent.getType() != current.getType()) { + if (parent.getType() != current.getType()) + { currentSub = newUnconstrainedVar(parent.getType(), currentSub); } current = parent; } - else { + else + { currentSub = Node(); } break; // Array select - if array is unconstrained, so is result case kind::SELECT: - if (parent[0] == current) { + if (parent[0] == current) + { ++d_numUnconstrainedElim; Assert(current.getType().isArray()); - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } - currentSub = newUnconstrainedVar(current.getType().getArrayConstituentType(), currentSub); + currentSub = newUnconstrainedVar( + current.getType().getArrayConstituentType(), currentSub); current = parent; } break; - // Array store - if both store and value are unconstrained, so is resulting store + // Array store - if both store and value are unconstrained, so is + // resulting store case kind::STORE: - if (((parent[0] == current && - d_unconstrained.find(parent[2]) != d_unconstrained.end()) || - (parent[2] == current && - d_unconstrained.find(parent[0]) != d_unconstrained.end()))) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (((parent[0] == current + && d_unconstrained.find(parent[2]) != d_unconstrained.end()) + || (parent[2] == current + && d_unconstrained.find(parent[0]) + != d_unconstrained.end()))) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (parent[0] != current) { - if (parent[0].isVar()) { + if (parent[0] != current) + { + if (parent[0].isVar()) + { currentSub = parent[0]; } - else { + else + { Assert(d_substitutions.hasSubstitution(parent[0])); currentSub = d_substitutions.apply(parent[0]); } } - else if (currentSub.isNull()) { + else if (currentSub.isNull()) + { currentSub = current; } current = parent; } - else { + else + { currentSub = Node(); } } @@ -531,24 +651,19 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_SLT: case kind::BITVECTOR_SGE: case kind::BITVECTOR_SGT: - case kind::BITVECTOR_SLE: { + case kind::BITVECTOR_SLE: + { // Tuples over (signed, swap, strict). - switch (parent.getKind()) { - case kind::BITVECTOR_UGE: - break; - case kind::BITVECTOR_ULT: - strict = true; - break; - case kind::BITVECTOR_ULE: - swap = true; - break; + switch (parent.getKind()) + { + case kind::BITVECTOR_UGE: break; + case kind::BITVECTOR_ULT: strict = true; break; + case kind::BITVECTOR_ULE: swap = true; break; case kind::BITVECTOR_UGT: swap = true; strict = true; break; - case kind::BITVECTOR_SGE: - isSigned = true; - break; + case kind::BITVECTOR_SGE: isSigned = true; break; case kind::BITVECTOR_SLT: isSigned = true; strict = true; @@ -562,54 +677,62 @@ void UnconstrainedSimplifier::processUnconstrained() swap = true; strict = true; break; - default: - Unreachable(); + default: Unreachable(); } TNode other; bool left = false; - if (parent[0] == current) { + if (parent[0] == current) + { other = parent[1]; left = true; - } else { + } + else + { Assert(parent[1] == current); other = parent[0]; } - if (d_unconstrained.find(other) != d_unconstrained.end()) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (d_unconstrained.find(other) != d_unconstrained.end()) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; - } else { + } + else + { currentSub = Node(); } - } else { + } + else + { unsigned size = current.getType().getBitVectorSize(); BitVector bv = isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) : BitVector(size, unsigned(0)); - if (swap == left) { + if (swap == left) + { bv = ~bv; } - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; - NodeManager* nm = NodeManager::currentNM(); Node test = Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); - if (test == nm->mkConst<bool>(false)) { + if (test == nm->mkConst<bool>(false)) + { break; } - if (strict) { - currentSub = currentSub.andNode(test.notNode()); - } else { - currentSub = currentSub.orNode(test); - } + currentSub = strict ? currentSub.andNode(test.notNode()) + : currentSub.orNode(test); // Delay adding this substitution - see comment at end of function delayQueueLeft.push_back(current); delayQueueRight.push_back(currentSub); @@ -619,40 +742,46 @@ void UnconstrainedSimplifier::processUnconstrained() break; } - // Do nothing + // Do nothing case kind::BITVECTOR_SIGN_EXTEND: case kind::BITVECTOR_ZERO_EXTEND: case kind::BITVECTOR_REPEAT: case kind::BITVECTOR_ROTATE_LEFT: case kind::BITVECTOR_ROTATE_RIGHT: - default: - break; + default: break; } - if( checkParent ){ - //run for various cases from above - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { + if (checkParent) + { + // run for various cases from above + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { ++d_numUnconstrainedElim; - if (currentSub.isNull()) { + if (currentSub.isNull()) + { currentSub = current; } current = parent; } - else { + else + { currentSub = Node(); } } - if (current == parent && d_visited[parent] == 1) { + if (current == parent && d_visited[parent] == 1) + { d_unconstrained.insert(parent); continue; } } - if (!currentSub.isNull()) { + if (!currentSub.isNull()) + { Assert(currentSub.isVar()); d_substitutions.addSubstitution(current, currentSub, false); } - if (workList.empty()) { + if (workList.empty()) + { break; } current = workList.back(); @@ -666,9 +795,11 @@ void UnconstrainedSimplifier::processUnconstrained() // substitution very quickly (never invalidating the substitution cache). // Bitvector comparisons are more complicated and may require // back-substitution and cache-invalidation. So we do these last. - while (!delayQueueLeft.empty()) { + while (!delayQueueLeft.empty()) + { left = delayQueueLeft.back(); - if (!d_substitutions.hasSubstitution(left)) { + if (!d_substitutions.hasSubstitution(left)) + { right = d_substitutions.apply(delayQueueRight.back()); d_substitutions.addSubstitution(delayQueueLeft.back(), right); } @@ -677,21 +808,27 @@ void UnconstrainedSimplifier::processUnconstrained() } } - -void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions) +PreprocessingPassResult UnconstrainedSimplifier::applyInternal( + AssertionPipeline* assertionsToPreprocess) { + d_preprocContext->spendResource(options::preprocessStep()); + + std::vector<Node>& assertions = assertionsToPreprocess->ref(); + d_context->push(); - vector<Node>::iterator it = assertions.begin(), iend = assertions.end(); - for (; it != iend; ++it) { - visitAll(*it); + for (const Node& assertion : assertions) + { + visitAll(assertion); } - if (!d_unconstrained.empty()) { + if (!d_unconstrained.empty()) + { processUnconstrained(); // d_substitutions.print(Message.getStream()); - for (it = assertions.begin(); it != iend; ++it) { - (*it) = Rewriter::rewrite(d_substitutions.apply(*it)); + for (Node& assertion : assertions) + { + assertion = Rewriter::rewrite(d_substitutions.apply(assertion)); } } @@ -701,4 +838,10 @@ void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions) d_visited.clear(); d_visitedOnce.clear(); d_unconstrained.clear(); + + return PreprocessingPassResult::NO_CONFLICT; } + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/theory/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index b13311e2a..658834ee3 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -11,37 +11,48 @@ ** ** \brief Simplifications based on unconstrained variables ** - ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions - ** by variables. Based on Roberto Bruttomesso's PhD thesis. + ** This module implements a preprocessing phase which replaces certain + ** "unconstrained" expressions by variables. Based on Roberto + ** Bruttomesso's PhD thesis. **/ #include "cvc4_private.h" -#ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H -#define __CVC4__UNCONSTRAINED_SIMPLIFIER_H +#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H #include <unordered_map> #include <unordered_set> -#include <utility> #include <vector> +#include "context/context.h" #include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/logic_info.h" #include "theory/substitutions.h" #include "util/statistics_registry.h" namespace CVC4 { +namespace preprocessing { +namespace passes { -/* Forward Declarations */ -class LogicInfo; +class UnconstrainedSimplifier : public PreprocessingPass +{ + public: + UnconstrainedSimplifier(PreprocessingPassContext* preprocContext); + ~UnconstrainedSimplifier() override; -class UnconstrainedSimplifier { + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + private: /** number of expressions eliminated due to unconstrained simplification */ IntStat d_numUnconstrainedElim; - typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; - typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + using TNodeCountMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>; + using TNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>; + using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; TNodeCountMap d_visited; TNodeMap d_visitedOnce; @@ -55,13 +66,10 @@ class UnconstrainedSimplifier { void visitAll(TNode assertion); Node newUnconstrainedVar(TypeNode t, TNode var); void processUnconstrained(); - -public: - UnconstrainedSimplifier(context::Context* context, const LogicInfo& logicInfo); - ~UnconstrainedSimplifier(); - void processAssertions(std::vector<Node>& assertions); }; -} +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 #endif diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index 97fa32d17..4143f2d4b 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -39,6 +39,7 @@ #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_engine_scope.h" #include "smt/term_formula_removal.h" +#include "theory/logic_info.h" #include "theory/substitutions.h" namespace CVC4 { diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index a289752fa..96e554680 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -43,6 +43,7 @@ class PreprocessingPassContext DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; } prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; } context::Context* getUserContext() { return d_smt->d_userContext; } + context::Context* getDecisionContext() { return d_smt->d_context; } RemoveTermFormulas* getIteRemover() { return d_iteRemover; } void spendResource(unsigned amount) @@ -50,6 +51,8 @@ class PreprocessingPassContext d_resourceManager->spendResource(amount); } + const LogicInfo& getLogicInfo() { return d_smt->d_logic; } + /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c4492d3a1..02e9892e2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -83,7 +83,10 @@ #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/ite_removal.h" #include "preprocessing/passes/ite_simp.h" +#include "preprocessing/passes/nl_ext_purify.h" #include "preprocessing/passes/pseudo_boolean_processor.h" +#include "preprocessing/passes/quantifier_macros.h" +#include "preprocessing/passes/quantifier_macros.h" #include "preprocessing/passes/quantifiers_preprocess.h" #include "preprocessing/passes/real_to_int.h" #include "preprocessing/passes/rewrite.h" @@ -94,6 +97,7 @@ #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/passes/synth_rew_rules.h" +#include "preprocessing/passes/unconstrained_simplifier.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "preprocessing/preprocessing_pass_registry.h" @@ -117,7 +121,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/ce_guided_instantiation.h" @@ -202,8 +205,6 @@ struct SmtEngineStatistics { IntStat d_numMiplibAssertionsRemoved; /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; - /** time spent in simplifying ITEs */ - TimerStat d_unconstrainedSimpTime; /** time spent in theory preprocessing */ TimerStat d_theoryPreprocessTime; /** time spent converting to CNF */ @@ -236,7 +237,6 @@ struct SmtEngineStatistics { d_miplibPassTime("smt::SmtEngine::miplibPassTime"), d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0), d_numConstantProps("smt::SmtEngine::numConstantProps", 0), - d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), @@ -255,7 +255,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->registerStat(&d_miplibPassTime); smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->registerStat(&d_numConstantProps); - smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); smtStatisticsRegistry()->registerStat(&d_numAssertionsPre); @@ -276,7 +275,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); - smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre); @@ -567,14 +565,6 @@ class SmtEnginePrivate : public NodeManagerListener { bool nonClausalSimplify(); /** - * Performs static learning on the assertions. - */ - void staticLearning(); - - Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq); - Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false); - - /** * Helper function to fix up assertion list to restore invariants needed after * ite removal. */ @@ -586,9 +576,6 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); - // Simplify based on unconstrained values - void unconstrainedSimp(); - /** * Trace nodes back to their assertions using CircuitPropagator's * BackEdgesMap. @@ -790,7 +777,7 @@ class SmtEnginePrivate : public NodeManagerListener { /** Process a user push. */ void notifyPush() { - + } /** @@ -872,13 +859,13 @@ class SmtEnginePrivate : public NodeManagerListener { std::ostream* getReplayLog() const { return d_managedReplayLog.getReplayLog(); } - + //------------------------------- expression names // implements setExpressionName, as described in smt_engine.h void setExpressionName(Expr e, std::string name) { d_exprNames[Node::fromExpr(e)] = name; } - + // implements getExpressionName, as described in smt_engine.h bool getExpressionName(Expr e, std::string& name) const { context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e); @@ -2026,7 +2013,6 @@ void SmtEngine::setDefaults() { } if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)) { - options::cbqiAll.set( false ); if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } @@ -2658,6 +2644,8 @@ void SmtEnginePrivate::finishInit() new IntToBV(d_preprocessingPassContext.get())); std::unique_ptr<ITESimp> iteSimp( new ITESimp(d_preprocessingPassContext.get())); + std::unique_ptr<NlExtPurify> nlExtPurify( + new NlExtPurify(d_preprocessingPassContext.get())); std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess( new QuantifiersPreprocess(d_preprocessingPassContext.get())); std::unique_ptr<PseudoBooleanProcessor> pbProc( @@ -2681,6 +2669,8 @@ void SmtEnginePrivate::finishInit() new SynthRewRulesPass(d_preprocessingPassContext.get())); std::unique_ptr<SepSkolemEmp> sepSkolemEmp( new SepSkolemEmp(d_preprocessingPassContext.get())); + std::unique_ptr<UnconstrainedSimplifier> unconstrainedSimplifier( + new UnconstrainedSimplifier(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("apply-substs", std::move(applySubsts)); d_preprocessingPassRegistry.registerPass("apply-to-const", @@ -2692,6 +2682,8 @@ void SmtEnginePrivate::finishInit() std::move(bvAckermann)); d_preprocessingPassRegistry.registerPass("bv-eager-atoms", std::move(bvEagerAtoms)); + std::unique_ptr<QuantifierMacros> quantifierMacros( + new QuantifierMacros(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); d_preprocessingPassRegistry.registerPass("bv-intro-pow2", std::move(bvIntroPow2)); @@ -2701,6 +2693,8 @@ void SmtEnginePrivate::finishInit() std::move(globalNegate)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp)); + d_preprocessingPassRegistry.registerPass("nl-ext-purify", + std::move(nlExtPurify)); d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", std::move(quantifiersPreprocess)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", @@ -2713,12 +2707,16 @@ void SmtEnginePrivate::finishInit() std::move(sepSkolemEmp)); d_preprocessingPassRegistry.registerPass("sort-inference", std::move(sortInfer)); - d_preprocessingPassRegistry.registerPass("static-learning", + d_preprocessingPassRegistry.registerPass("static-learning", std::move(staticLearning)); d_preprocessingPassRegistry.registerPass("sygus-infer", std::move(sygusInfer)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc)); + d_preprocessingPassRegistry.registerPass("quantifier-macros", + std::move(quantifierMacros)); + d_preprocessingPassRegistry.registerPass("unconstrained-simplifier", + std::move(unconstrainedSimplifier)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) @@ -2904,68 +2902,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node return result.top(); } -typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; - -Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector< Node >& var_eq, bool beneathMult) { - if( beneathMult ){ - NodeMap::iterator find = bcache.find(n); - if (find != bcache.end()) { - return (*find).second; - } - }else{ - NodeMap::iterator find = cache.find(n); - if (find != cache.end()) { - return (*find).second; - } - } - Node ret = n; - if( n.getNumChildren()>0 ){ - if (beneathMult - && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) - { - // don't do it if it rewrites to a constant - Node nr = Rewriter::rewrite(n); - if (nr.isConst()) - { - // return the rewritten constant - ret = nr; - } - else - { - // new variable - ret = NodeManager::currentNM()->mkSkolem( - "__purifyNl_var", - n.getType(), - "Variable introduced in purifyNl pass"); - Node np = purifyNlTerms(n, cache, bcache, var_eq, false); - var_eq.push_back(np.eqNode(ret)); - Trace("nl-ext-purify") - << "Purify : " << ret << " -> " << np << std::endl; - } - } - else - { - bool beneathMultNew = beneathMult || n.getKind()==kind::MULT; - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node nc = purifyNlTerms( n[i], cache, bcache, var_eq, beneathMultNew ); - childChanged = childChanged || nc!=n[i]; - children.push_back( nc ); - } - if( childChanged ){ - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - } - if( beneathMult ){ - bcache[n] = ret; - }else{ - cache[n] = ret; - } - return ret; -} - // do dumping (before/after any preprocessing pass) static void dumpAssertions(const char* key, const AssertionPipeline& assertionList) { @@ -3316,13 +3252,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } -void SmtEnginePrivate::unconstrainedSimp() { - TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); - spendResource(options::preprocessStep()); - Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; - d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref()); -} - void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) { const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) { @@ -3806,14 +3735,10 @@ bool SmtEnginePrivate::simplifyAssertions() // Unconstrained simplification if(options::unconstrainedSimp()) { - Chat() << "...doing unconstrained simplification..." << endl; - unconstrainedSimp(); + d_preprocessingPassRegistry.getPass("unconstrained-simplifier") + ->apply(&d_assertions); } - dumpAssertions("post-unconstrained", d_assertions); - Trace("smt") << "POST unconstrainedSimp" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -4038,20 +3963,7 @@ void SmtEnginePrivate::processAssertions() { } if( options::nlExtPurify() ){ - unordered_map<Node, Node, NodeHashFunction> cache; - unordered_map<Node, Node, NodeHashFunction> bcache; - std::vector< Node > var_eq; - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Node a = d_assertions[i]; - d_assertions.replace(i, purifyNlTerms(a, cache, bcache, var_eq)); - Trace("nl-ext-purify") - << "Purify : " << a << " -> " << d_assertions[i] << std::endl; - } - if( !var_eq.empty() ){ - unsigned lastIndex = d_assertions.size()-1; - var_eq.insert( var_eq.begin(), d_assertions[lastIndex] ); - d_assertions.replace(lastIndex, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) ); - } + d_preprocessingPassRegistry.getPass("nl-ext-purify")->apply(&d_assertions); } if( options::ceGuidedInst() ){ @@ -4101,12 +4013,9 @@ void SmtEnginePrivate::processAssertions() { // Unconstrained simplification if(options::unconstrainedSimp()) { - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; - dumpAssertions("pre-unconstrained-simp", d_assertions); d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); - unconstrainedSimp(); - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl; - dumpAssertions("post-unconstrained-simp", d_assertions); + d_preprocessingPassRegistry.getPass("unconstrained-simplifier") + ->apply(&d_assertions); } if(options::bvIntroducePow2()) @@ -4157,13 +4066,8 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-skolem-quant", d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion - quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() ); - bool success; - do{ - success = qm.simplify( d_assertions.ref(), true ); - }while( success ); - //finalize the definitions - qm.finalizeDefinitions(); + d_preprocessingPassRegistry.getPass("quantifier-macros") + ->apply(&d_assertions); } //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF @@ -5528,7 +5432,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) Assert( inst_qs.size()<=1 ); Node ret_n; if( inst_qs.size()==1 ){ - Node top_q = inst_qs[0]; + Node top_q = inst_qs[0]; //Node top_q = Rewriter::rewrite( nn_e ).negate(); Assert( top_q.getKind()==kind::FORALL ); Trace("smt-qe") << "Get qe for " << top_q << std::endl; @@ -5951,7 +5855,7 @@ void SmtEngine::setReplayStream(ExprStream* replayStream) { AlwaysAssert(!d_fullyInited, "Cannot set replay stream once fully initialized"); d_replayStream = replayStream; -} +} bool SmtEngine::getExpressionName(Expr e, std::string& name) const { return d_private->getExpressionName(e, name); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 65df3a642..283c70ada 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -41,24 +41,26 @@ namespace CVC4 { namespace theory { namespace datatypes { -TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo) +TheoryDatatypes::TheoryDatatypes(Context* c, + UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), - //d_cycle_check(c), - d_hasSeenCycle(c, false), d_infer(c), d_infer_exp(c), - d_term_sk( u ), - d_notify( *this ), + d_term_sk(u), + d_notify(*this), d_equalityEngine(d_notify, c, "theory::datatypes", true), - d_labels( c ), - d_selector_apps( c ), - //d_consEqc( c ), - d_conflict( c, false ), - d_collectTermsCache( c ), - d_functionTerms( c ), - d_singleton_eq( u ), - d_lemmas_produced_c( u ) + d_labels(c), + d_selector_apps(c), + d_conflict(c, false), + d_addedLemma(false), + d_addedFact(false), + d_collectTermsCache(c), + d_functionTerms(c), + d_singleton_eq(u), + d_lemmas_produced_c(u) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -765,25 +767,6 @@ void TheoryDatatypes::conflict(TNode a, TNode b){ void TheoryDatatypes::eqNotifyNewClass(TNode t){ if( t.getKind()==APPLY_CONSTRUCTOR ){ getOrMakeEqcInfo( t, true ); - //look at all equivalence classes with constructor terms -/* - for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){ - if( (*it).second ){ - TNode r = (*it).first; - if( r.getType()==t.getType() ){ - EqcInfo * ei = getOrMakeEqcInfo( r, false ); - if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){ - Node deq = ei->d_constructor.get().eqNode( t ).negate(); - d_pending.push_back( deq ); - d_pending_exp[ deq ] = d_true; - Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl; - d_infer.push_back( deq ); - } - } - } - } -*/ - //d_consEqc[t] = true; } } @@ -865,14 +848,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( d_conflict ){ return; } - //d_consEqc[t1] = true; } - //AJR: do this? - //else if( cons2.isConst() ){ - // //prefer the constant - // eqc1->d_constructor = cons2; - //} - //d_consEqc[t2] = false; } }else{ Trace("datatypes-debug") << " no eqc info for " << t1 << ", must create" << std::endl; @@ -1998,9 +1974,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, for( unsigned i=0; i<ncons.getNumChildren(); i++ ) { TNode cn = searchForCycle( ncons[i], on, visited, proc, explanation, false ); if( cn==on ) { - //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){ - // Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl; - //} //add explanation for why the constructor is connected if( n != ncons ) { explainEquality( n, ncons, true, explanation ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index e06bb7408..233ebd052 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -46,10 +46,6 @@ class TheoryDatatypes : public Theory { typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; - /** transitive closure to record equivalence/subterm relation. */ - // TransitiveClosureNode d_cycle_check; - /** has seen cycle */ - context::CDO<bool> d_hasSeenCycle; /** inferences */ NodeList d_infer; NodeList d_infer_exp; @@ -179,12 +175,19 @@ private: /** selector apps for eqch equivalence class */ NodeIntMap d_selector_apps; std::map< Node, std::vector< Node > > d_selector_apps_data; - /** constructor terms */ - //BoolMap d_consEqc; /** Are we in conflict */ context::CDO<bool> d_conflict; - /** Added lemma ? */ + /** added lemma + * + * This flag is set to true during a full effort check if this theory + * called d_out->lemma(...). + */ bool d_addedLemma; + /** added fact + * + * This flag is set to true during a full effort check if this theory + * added an internal fact to its equality engine. + */ bool d_addedFact; /** The conflict node */ Node d_conflictNode; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 83098e3ba..3cf605238 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -57,7 +57,7 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery }; BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn) - : Instantiator(qe, tn) + : Instantiator(qe, tn), d_inst_id_counter(0) { // get the global inverter utility // this must be global since we need to: diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index c281e81ca..ac76ee31f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -38,11 +38,14 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA -InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), -d_elim_quants( qe->getSatContext() ), -d_nested_qe_waitlist_size( qe->getUserContext() ), -d_nested_qe_waitlist_proc( qe->getUserContext() ) +InstStrategyCbqi::InstStrategyCbqi(QuantifiersEngine* qe) + : QuantifiersModule(qe), + d_cbqi_set_quant_inactive(false), + d_incomplete_check(false), + d_added_cbqi_lemma(qe->getUserContext()), + d_elim_quants(qe->getSatContext()), + d_nested_qe_waitlist_size(qe->getUserContext()), + d_nested_qe_waitlist_proc(qe->getUserContext()) //, d_added_inst( qe->getUserContext() ) { d_qid_count = 0; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 236904ef2..4334652da 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -37,7 +37,18 @@ class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; protected: + /** set quantified formula inactive + * + * This flag is set to true during a full effort check if at least one + * quantified formula is set "inactive", that is, its negation is + * unsatisfiable in the current context. + */ bool d_cbqi_set_quant_inactive; + /** incomplete check + * + * This is set to true during a full effort check if this strategy could + * not find an instantiation for at least one asserted quantified formula. + */ bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index e82ab617a..a1c132fda 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -80,16 +80,18 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& } } - - -ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), -d_notify( *this ), -d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), -d_ee_conjectures( c ){ - d_fullEffortCount = 0; - d_conj_count = 0; - d_subs_confirmCount = 0; - d_subs_unkCount = 0; +ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe, + context::Context* c) + : QuantifiersModule(qe), + d_notify(*this), + d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), + d_ee_conjectures(c), + d_conj_count(0), + d_subs_confirmCount(0), + d_subs_unkCount(0), + d_fullEffortCount(0), + d_hasAddedLemma(false) +{ d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR ); diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 6d626038d..a3a0b8795 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -70,10 +70,19 @@ class TermGenEnv; class TermGenerator { -private: + private: unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs ); -public: - TermGenerator(){} + + public: + TermGenerator() + : d_id(0), + d_status(0), + d_status_num(0), + d_match_status(0), + d_match_status_child_num(0), + d_match_mode(0) + { + } TypeNode d_typ; unsigned d_id; //1 : consider as unique variable diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 4208b11ae..6ea6e50b3 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -33,8 +33,9 @@ bool CandidateGenerator::isLegalCandidate( Node n ){ return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); } -CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) : -CandidateGenerator( qe ), d_term_iter( -1 ){ +CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat) + : CandidateGenerator(qe), d_term_iter(-1), d_term_iter_limit(0) +{ d_op = qe->getTermDatabase()->getMatchOperator( pat ); Assert( !d_op.isNull() ); } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index a8079f775..1e3116f43 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -572,10 +572,6 @@ void FirstOrderModelIG::resetEvaluate(){ d_eval_uf_use_default.clear(); d_eval_uf_model.clear(); d_eval_term_index_order.clear(); - d_eval_formulas = 0; - d_eval_uf_terms = 0; - d_eval_lits = 0; - d_eval_lits_unknown = 0; } //if evaluate( n ) = eVal, @@ -585,7 +581,6 @@ void FirstOrderModelIG::resetEvaluate(){ // if eVal is not 0, then // each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ - ++d_eval_formulas; Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl; //Notice() << "Eval " << n << std::endl; if( n.getKind()==NOT ){ @@ -661,7 +656,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ }else if( n.getKind()==FORALL ){ return 0; }else{ - ++d_eval_lits; //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; int retVal = 0; depIndex = ri->getNumTerms()-1; @@ -684,7 +678,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ if( retVal!=0 ){ Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl; }else{ - ++d_eval_lits_unknown; Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; Trace("fmf-eval-amb") << " value : " << val << std::endl; } @@ -731,7 +724,6 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; //if it is a defined UF, then consult the interpretation if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ - ++d_eval_uf_terms; int argDepIndex = 0; //make the term model specifically for n makeEvalUfModel( n ); diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 059250f8d..7da5b2088 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -266,12 +266,6 @@ public: /** evaluate functions */ int evaluate( Node n, int& depIndex, RepSetIterator* ri ); Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ); -public: - //statistics - int d_eval_formulas; - int d_eval_uf_terms; - int d_eval_lits; - int d_eval_lits_unknown; private: //default evaluate term function Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index d1b7eebb8..c03fc7a32 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -457,24 +457,17 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){ return false; } -QModelBuilderIG::Statistics::Statistics(): - d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), - d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0), - d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ), - d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ), - d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ), - d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ), - d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ), - d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 ) +QModelBuilderIG::Statistics::Statistics() + : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), + d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", + 0), + d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0), + d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0) { smtStatisticsRegistry()->registerStat(&d_num_quants_init); smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init); smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas); smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas); - smtStatisticsRegistry()->registerStat(&d_eval_formulas); - smtStatisticsRegistry()->registerStat(&d_eval_uf_terms); - smtStatisticsRegistry()->registerStat(&d_eval_lits); - smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown); } QModelBuilderIG::Statistics::~Statistics(){ @@ -482,10 +475,6 @@ QModelBuilderIG::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init); smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas); smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_eval_formulas); - smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms); - smtStatisticsRegistry()->unregisterStat(&d_eval_lits); - smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown); } //do exhaustive instantiation @@ -558,12 +547,6 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in } } //print debugging information - if( fmig ){ - d_statistics.d_eval_formulas += fmig->d_eval_formulas; - d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms; - d_statistics.d_eval_lits += fmig->d_eval_lits; - d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown; - } Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl; Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl; Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl; diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 353883a20..b34f1e580 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -148,10 +148,6 @@ class QModelBuilderIG : public QModelBuilder IntStat d_num_partial_quants_init; IntStat d_init_inst_gen_lemmas; IntStat d_inst_gen_lemmas; - IntStat d_eval_formulas; - IntStat d_eval_uf_terms; - IntStat d_eval_lits; - IntStat d_eval_lits_unknown; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h deleted file mode 100644 index b36be7aec..000000000 --- a/src/theory/quantifiers/macros.h +++ /dev/null @@ -1,74 +0,0 @@ -/********************* */ -/*! \file macros.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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.\endverbatim - ** - ** \brief Pre-process step for detecting quantifier macro definitions - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__QUANTIFIERS_MACROS_H -#define __CVC4__QUANTIFIERS_MACROS_H - -#include <iostream> -#include <string> -#include <vector> -#include <map> -#include "expr/node.h" -#include "expr/type_node.h" -#include "theory/quantifiers_engine.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class QuantifierMacros{ -private: - QuantifiersEngine * d_qe; -private: - bool d_ground_macros; - bool processAssertion( Node n ); - bool isBoundVarApplyUf( Node n ); - bool process( Node n, bool pol, std::vector< Node >& args, Node f ); - bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ); - bool isMacroLiteral( Node n, bool pol ); - bool isGroundUfTerm( Node f, Node n ); - void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ); - Node solveInEquality( Node n, Node lit ); - bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ); - bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, - std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ); - //map from operators to macro basis terms - std::map< Node, std::vector< Node > > d_macro_basis; - //map from operators to macro definition - std::map< Node, Node > d_macro_defs; - std::map< Node, Node > d_macro_defs_new; - //operators to macro ops that contain them - std::map< Node, std::vector< Node > > d_macro_def_contains; - //simplify caches - std::map< Node, Node > d_simplify_cache; - std::map< Node, bool > d_quant_macros; -private: - Node simplify( Node n ); - void addMacro( Node op, Node n, std::vector< Node >& opc ); - void debugMacroDefinition( Node oo, Node n ); -public: - QuantifierMacros( QuantifiersEngine * qe ); - ~QuantifierMacros(){} - - bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); - void finalizeDefinitions(); -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a5cd95d29..510953035 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -70,10 +70,36 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te) : d_te(te), + d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), + d_eq_inference(nullptr), + d_inst_prop(nullptr), + d_tr_trie(new inst::TriggerTrie), + d_model(nullptr), + d_quant_rel(nullptr), + d_rel_dom(nullptr), + d_bv_invert(nullptr), + d_builder(nullptr), + d_qepr(nullptr), + d_term_util(new quantifiers::TermUtil(this)), + d_term_db(new quantifiers::TermDb(c, u, this)), + d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), d_instantiate(new quantifiers::Instantiate(this, u)), d_skolemize(new quantifiers::Skolemize(this, u)), d_term_enum(new quantifiers::TermEnumeration), + d_alpha_equiv(nullptr), + d_inst_engine(nullptr), + d_model_engine(nullptr), + d_bint(nullptr), + d_qcf(nullptr), + d_rr_engine(nullptr), + d_sg_gen(nullptr), + d_ceg_inst(nullptr), + d_lte_part_inst(nullptr), + d_fs(nullptr), + d_i_cbqi(nullptr), + d_qsplit(nullptr), + d_anti_skolem(nullptr), d_conflict_c(c, false), // d_quants(u), d_quants_prereg(u), @@ -89,41 +115,29 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_presolve_cache_wq(u), d_presolve_cache_wic(u) { - //utilities - d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this ); - d_util.push_back( d_eq_query ); + //---- utilities + d_util.push_back(d_eq_query.get()); + // term util must come before the other utilities + d_util.push_back(d_term_util.get()); + d_util.push_back(d_term_db.get()); - // term util must come first - d_term_util = new quantifiers::TermUtil(this); - d_util.push_back(d_term_util); - - d_term_db = new quantifiers::TermDb( c, u, this ); - d_util.push_back( d_term_db ); - if (options::ceGuidedInst()) { - d_sygus_tdb = new quantifiers::TermDbSygus(c, this); - }else{ - d_sygus_tdb = NULL; + d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this)); } if( options::instPropagate() ){ // notice that this option is incompatible with options::qcfAllConflict() - d_inst_prop = new quantifiers::InstPropagator( this ); - d_util.push_back( d_inst_prop ); + d_inst_prop.reset(new quantifiers::InstPropagator(this)); + d_util.push_back(d_inst_prop.get()); d_instantiate->addNotify(d_inst_prop->getInstantiationNotify()); - }else{ - d_inst_prop = NULL; } if( options::inferArithTriggerEq() ){ - d_eq_inference = new quantifiers::EqualityInference(c, false); - }else{ - d_eq_inference = NULL; + d_eq_inference.reset(new quantifiers::EqualityInference(c, false)); } d_util.push_back(d_instantiate.get()); - d_tr_trie = new inst::TriggerTrie; d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; d_conflict = false; d_hasAddedLemma = false; @@ -135,37 +149,15 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; if( options::relevantTriggers() ){ - d_quant_rel = new quantifiers::QuantRelevance; - d_util.push_back(d_quant_rel); - }else{ - d_quant_rel = NULL; + d_quant_rel.reset(new quantifiers::QuantRelevance); + d_util.push_back(d_quant_rel.get()); } if( options::quantEpr() ){ Assert( !options::incrementalSolving() ); - d_qepr = new quantifiers::QuantEPR; - }else{ - d_qepr = NULL; + d_qepr.reset(new quantifiers::QuantEPR); } - - - d_qcf = NULL; - d_sg_gen = NULL; - d_inst_engine = NULL; - d_i_cbqi = NULL; - d_qsplit = NULL; - d_anti_skolem = NULL; - d_model = NULL; - d_model_engine = NULL; - d_bint = NULL; - d_rr_engine = NULL; - d_ceg_inst = NULL; - d_lte_part_inst = NULL; - d_alpha_equiv = NULL; - d_fs = NULL; - d_rel_dom = NULL; - d_bv_invert = NULL; - d_builder = NULL; + //---- end utilities //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; @@ -178,70 +170,70 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, bool needsRelDom = false; //add quantifiers modules if( options::quantConflictFind() || options::quantRewriteRules() ){ - d_qcf = new quantifiers::QuantConflictFind( this, c); - d_modules.push_back( d_qcf ); + d_qcf.reset(new quantifiers::QuantConflictFind(this, c)); + d_modules.push_back(d_qcf.get()); } if( options::conjectureGen() ){ - d_sg_gen = new quantifiers::ConjectureGenerator( this, c ); - d_modules.push_back( d_sg_gen ); + d_sg_gen.reset(new quantifiers::ConjectureGenerator(this, c)); + d_modules.push_back(d_sg_gen.get()); } if( !options::finiteModelFind() || options::fmfInstEngine() ){ - d_inst_engine = new quantifiers::InstantiationEngine( this ); - d_modules.push_back( d_inst_engine ); + d_inst_engine.reset(new quantifiers::InstantiationEngine(this)); + d_modules.push_back(d_inst_engine.get()); } if( options::cbqi() ){ - d_i_cbqi = new quantifiers::InstStrategyCegqi( this ); - d_modules.push_back( d_i_cbqi ); + d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(this)); + d_modules.push_back(d_i_cbqi.get()); if( options::cbqiBv() ){ // if doing instantiation for BV, need the inverter class - d_bv_invert = new quantifiers::BvInverter; + d_bv_invert.reset(new quantifiers::BvInverter); } } if( options::ceGuidedInst() ){ - d_ceg_inst = new quantifiers::CegInstantiation( this, c ); - d_modules.push_back( d_ceg_inst ); + d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c)); + d_modules.push_back(d_ceg_inst.get()); //needsBuilder = true; } //finite model finding if( options::finiteModelFind() ){ if( options::fmfBound() ){ - d_bint = new quantifiers::BoundedIntegers( c, this ); - d_modules.push_back( d_bint ); + d_bint.reset(new quantifiers::BoundedIntegers(c, this)); + d_modules.push_back(d_bint.get()); } - d_model_engine = new quantifiers::ModelEngine( c, this ); - d_modules.push_back( d_model_engine ); + d_model_engine.reset(new quantifiers::ModelEngine(c, this)); + d_modules.push_back(d_model_engine.get()); //finite model finder has special ways of building the model needsBuilder = true; } if( options::quantRewriteRules() ){ - d_rr_engine = new quantifiers::RewriteEngine( c, this ); - d_modules.push_back(d_rr_engine); + d_rr_engine.reset(new quantifiers::RewriteEngine(c, this)); + d_modules.push_back(d_rr_engine.get()); } if( options::ltePartialInst() ){ - d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); - d_modules.push_back( d_lte_part_inst ); + d_lte_part_inst.reset(new quantifiers::LtePartialInst(this, c)); + d_modules.push_back(d_lte_part_inst.get()); } if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){ - d_qsplit = new quantifiers::QuantDSplit( this, c ); - d_modules.push_back( d_qsplit ); + d_qsplit.reset(new quantifiers::QuantDSplit(this, c)); + d_modules.push_back(d_qsplit.get()); } if( options::quantAntiSkolem() ){ - d_anti_skolem = new quantifiers::QuantAntiSkolem( this ); - d_modules.push_back( d_anti_skolem ); + d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(this)); + d_modules.push_back(d_anti_skolem.get()); } if( options::quantAlphaEquiv() ){ - d_alpha_equiv = new quantifiers::AlphaEquivalence( this ); + d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(this)); } //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){ - d_fs = new quantifiers::InstStrategyEnum(this); - d_modules.push_back( d_fs ); + d_fs.reset(new quantifiers::InstStrategyEnum(this)); + d_modules.push_back(d_fs.get()); needsRelDom = true; } if( needsRelDom ){ - d_rel_dom = new quantifiers::RelevantDomain( this ); - d_util.push_back( d_rel_dom ); + d_rel_dom.reset(new quantifiers::RelevantDomain(this)); + d_util.push_back(d_rel_dom.get()); } // if we require specialized ways of building the model @@ -252,53 +244,27 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, || options::fmfBound()) { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; - d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); - d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); + d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( + this, c, "FirstOrderModelFmc")); + d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this)); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl; - d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" ); - d_builder = new quantifiers::AbsMbqiBuilder( c, this ); + d_model.reset( + new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs")); + d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; - d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); - d_builder = new quantifiers::QModelBuilderDefault( c, this ); + d_model.reset( + new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); + d_builder.reset(new quantifiers::QModelBuilderDefault(c, this)); } }else{ - d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); + d_model.reset( + new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); } } -QuantifiersEngine::~QuantifiersEngine() -{ - delete d_alpha_equiv; - delete d_builder; - delete d_qepr; - delete d_rr_engine; - delete d_bint; - delete d_model_engine; - delete d_inst_engine; - delete d_qcf; - delete d_quant_rel; - delete d_rel_dom; - delete d_bv_invert; - delete d_model; - delete d_tr_trie; - delete d_term_db; - delete d_sygus_tdb; - delete d_term_util; - delete d_eq_inference; - delete d_eq_query; - delete d_sg_gen; - delete d_ceg_inst; - delete d_lte_part_inst; - delete d_fs; - delete d_i_cbqi; - delete d_qsplit; - delete d_anti_skolem; - delete d_inst_prop; -} - -EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } +QuantifiersEngine::~QuantifiersEngine() {} context::Context* QuantifiersEngine::getSatContext() { @@ -325,6 +291,96 @@ const LogicInfo& QuantifiersEngine::getLogicInfo() const return d_te->getLogicInfo(); } +EqualityQuery* QuantifiersEngine::getEqualityQuery() const +{ + return d_eq_query.get(); +} +quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const +{ + return d_eq_inference.get(); +} +quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const +{ + return d_rel_dom.get(); +} +quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const +{ + return d_bv_invert.get(); +} +quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const +{ + return d_quant_rel.get(); +} +quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const +{ + return d_builder.get(); +} +quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const +{ + return d_qepr.get(); +} +quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const +{ + return d_model.get(); +} +quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const +{ + return d_term_db.get(); +} +quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const +{ + return d_sygus_tdb.get(); +} +quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const +{ + return d_term_util.get(); +} +quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const +{ + return d_quant_attr.get(); +} +quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const +{ + return d_instantiate.get(); +} +quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const +{ + return d_skolemize.get(); +} +quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const +{ + return d_term_enum.get(); +} +inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const +{ + return d_tr_trie.get(); +} + +quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const +{ + return d_bint.get(); +} +quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const +{ + return d_qcf.get(); +} +quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const +{ + return d_rr_engine.get(); +} +quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const +{ + return d_ceg_inst.get(); +} +quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const +{ + return d_fs.get(); +} +quantifiers::InstStrategyCbqi* QuantifiersEngine::getInstStrategyCbqi() const +{ + return d_i_cbqi.get(); +} + QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); if( it==d_owner.end() ){ @@ -419,7 +475,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ // if we want to use the model's equality engine, build the model now if( d_useModelEe && !d_model->isBuilt() ){ Trace("quant-engine-debug") << "Build the model." << std::endl; - if( !d_te->getModelBuilder()->buildModel( d_model ) ){ + if (!d_te->getModelBuilder()->buildModel(d_model.get())) + { //we are done if model building was unsuccessful flushLemmas(); if( d_hasAddedLemma ){ @@ -582,9 +639,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ { // theory engine's model builder is quantifier engine's builder if it // has one - Assert(!d_builder || d_builder == d_te->getModelBuilder()); + Assert(!getModelBuilder() + || getModelBuilder() == d_te->getModelBuilder()); Trace("quant-engine-debug") << "Build model..." << std::endl; - if (!d_te->getModelBuilder()->buildModel(d_model)) + if (!d_te->getModelBuilder()->buildModel(d_model.get())) { flushLemmas(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 674954023..aabca1640 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -84,134 +84,17 @@ namespace inst { class QuantifiersEngine { - // TODO: remove these github issue #1163 - friend class quantifiers::InstantiationEngine; - friend class quantifiers::InstStrategyCbqi; - friend class quantifiers::InstStrategyCegqi; - friend class quantifiers::ModelEngine; - friend class quantifiers::RewriteEngine; - friend class quantifiers::QuantConflictFind; - friend class inst::InstMatch; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; typedef context::CDList<Node> NodeList; typedef context::CDList<bool> BoolList; typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; -private: - /** reference to theory engine object */ - TheoryEngine* d_te; - /** vector of utilities for quantifiers */ - std::vector< QuantifiersUtil* > d_util; - /** vector of modules for quantifiers */ - std::vector< QuantifiersModule* > d_modules; - /** equality query class */ - quantifiers::EqualityQueryQuantifiersEngine* d_eq_query; - /** equality inference class */ - quantifiers::EqualityInference* d_eq_inference; - /** for computing relevance of quantifiers */ - quantifiers::QuantRelevance* d_quant_rel; - /** relevant domain */ - quantifiers::RelevantDomain* d_rel_dom; - /** inversion utility for BV instantiation */ - quantifiers::BvInverter * d_bv_invert; - /** alpha equivalence */ - quantifiers::AlphaEquivalence * d_alpha_equiv; - /** model builder */ - quantifiers::QModelBuilder* d_builder; - /** utility for effectively propositional logic */ - quantifiers::QuantEPR* d_qepr; - /** term database */ - quantifiers::TermDb* d_term_db; - /** sygus term database */ - quantifiers::TermDbSygus* d_sygus_tdb; - /** term utilities */ - quantifiers::TermUtil* d_term_util; - /** quantifiers attributes */ - std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; - /** instantiate utility */ - std::unique_ptr<quantifiers::Instantiate> d_instantiate; - /** skolemize utility */ - std::unique_ptr<quantifiers::Skolemize> d_skolemize; - /** term enumeration utility */ - std::unique_ptr<quantifiers::TermEnumeration> d_term_enum; - /** instantiation engine */ - quantifiers::InstantiationEngine* d_inst_engine; - /** model engine */ - quantifiers::ModelEngine* d_model_engine; - /** bounded integers utility */ - quantifiers::BoundedIntegers * d_bint; - /** Conflict find mechanism for quantifiers */ - quantifiers::QuantConflictFind* d_qcf; - /** rewrite rules utility */ - quantifiers::RewriteEngine * d_rr_engine; - /** subgoal generator */ - quantifiers::ConjectureGenerator * d_sg_gen; - /** ceg instantiation */ - quantifiers::CegInstantiation * d_ceg_inst; - /** lte partial instantiation */ - quantifiers::LtePartialInst * d_lte_part_inst; - /** full saturation */ - quantifiers::InstStrategyEnum* d_fs; - /** counterexample-based quantifier instantiation */ - quantifiers::InstStrategyCbqi * d_i_cbqi; - /** quantifiers splitting */ - quantifiers::QuantDSplit * d_qsplit; - /** quantifiers anti-skolemization */ - quantifiers::QuantAntiSkolem * d_anti_skolem; - /** quantifiers instantiation propagtor */ - quantifiers::InstPropagator * d_inst_prop; - - private: //this information is reset during check - /** current effort level */ - QuantifiersModule::QEffort d_curr_effort_level; - /** are we in conflict */ - bool d_conflict; - context::CDO<bool> d_conflict_c; - /** has added lemma this round */ - bool d_hasAddedLemma; - /** whether to use model equality engine */ - bool d_useModelEe; - private: - /** list of all quantifiers seen */ - std::map< Node, bool > d_quants; - /** quantifiers pre-registered */ - NodeSet d_quants_prereg; - /** quantifiers reduced */ - BoolMap d_quants_red; - std::map< Node, Node > d_quants_red_lem; - /** list of all lemmas produced */ - //std::map< Node, bool > d_lemmas_produced; - BoolMap d_lemmas_produced_c; - /** lemmas waiting */ - std::vector< Node > d_lemmas_waiting; - /** phase requirements waiting */ - std::map< Node, bool > d_phase_req_waiting; - /** all triggers will be stored in this trie */ - inst::TriggerTrie* d_tr_trie; - /** extended model object */ - quantifiers::FirstOrderModel* d_model; - /** inst round counters TODO: make context-dependent? */ - context::CDO< int > d_ierCounter_c; - int d_ierCounter; - int d_ierCounter_lc; - int d_ierCounterLastLc; - int d_inst_when_phase; - /** has presolve been called */ - context::CDO< bool > d_presolve; - /** presolve cache */ - NodeSet d_presolve_in; - NodeList d_presolve_cache; - BoolList d_presolve_cache_wq; - BoolList d_presolve_cache_wic; public: QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); ~QuantifiersEngine(); + //---------------------- external interface /** get theory engine */ - TheoryEngine* getTheoryEngine() { return d_te; } - /** get equality query */ - EqualityQuery* getEqualityQuery(); - /** get the equality inference */ - quantifiers::EqualityInference* getEqualityInference() { return d_eq_inference; } + TheoryEngine* getTheoryEngine() const { return d_te; } /** get default sat context for quantifiers engine */ context::Context* getSatContext(); /** get default sat context for quantifiers engine */ @@ -222,42 +105,56 @@ public: Valuation& getValuation(); /** get the logic info for the quantifiers engine */ const LogicInfo& getLogicInfo() const; + //---------------------- end external interface + //---------------------- utilities + /** get equality query */ + EqualityQuery* getEqualityQuery() const; + /** get the equality inference */ + quantifiers::EqualityInference* getEqualityInference() const; /** get relevant domain */ - quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; } + quantifiers::RelevantDomain* getRelevantDomain() const; /** get the BV inverter utility */ - quantifiers::BvInverter * getBvInverter() { return d_bv_invert; } + quantifiers::BvInverter* getBvInverter() const; /** get quantifier relevance */ - quantifiers::QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } + quantifiers::QuantRelevance* getQuantifierRelevance() const; /** get the model builder */ - quantifiers::QModelBuilder* getModelBuilder() { return d_builder; } + quantifiers::QModelBuilder* getModelBuilder() const; /** get utility for EPR */ - quantifiers::QuantEPR* getQuantEPR() { return d_qepr; } - public: // modules - /** get instantiation engine */ - quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } - /** get model engine */ - quantifiers::ModelEngine* getModelEngine() { return d_model_engine; } + quantifiers::QuantEPR* getQuantEPR() const; + /** get model */ + quantifiers::FirstOrderModel* getModel() const; + /** get term database */ + quantifiers::TermDb* getTermDatabase() const; + /** get term database sygus */ + quantifiers::TermDbSygus* getTermDatabaseSygus() const; + /** get term utilities */ + quantifiers::TermUtil* getTermUtil() const; + /** get quantifiers attributes */ + quantifiers::QuantAttributes* getQuantAttributes() const; + /** get instantiate utility */ + quantifiers::Instantiate* getInstantiate() const; + /** get skolemize utility */ + quantifiers::Skolemize* getSkolemize() const; + /** get term enumeration utility */ + quantifiers::TermEnumeration* getTermEnumeration() const; + /** get trigger database */ + inst::TriggerTrie* getTriggerDatabase() const; + //---------------------- end utilities + //---------------------- modules /** get bounded integers utility */ - quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; } + quantifiers::BoundedIntegers* getBoundedIntegers() const; /** Conflict find mechanism for quantifiers */ - quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; } + quantifiers::QuantConflictFind* getConflictFind() const; /** rewrite rules utility */ - quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; } - /** subgoal generator */ - quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; } + quantifiers::RewriteEngine* getRewriteEngine() const; /** ceg instantiation */ - quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } - /** local theory ext partial inst */ - quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } + quantifiers::CegInstantiation* getCegInstantiation() const; /** get full saturation */ - quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; } + quantifiers::InstStrategyEnum* getInstStrategyEnum() const; /** get inst strategy cbqi */ - quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; } - /** get quantifiers splitting */ - quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; } - /** get quantifiers anti-skolemization */ - quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; } -private: + quantifiers::InstStrategyCbqi* getInstStrategyCbqi() const; + //---------------------- end modules + private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; std::map< Node, int > d_owner_priority; @@ -331,29 +228,6 @@ public: /** get user pat mode */ quantifiers::UserPatMode getInstUserPatMode(); public: - /** get model */ - quantifiers::FirstOrderModel* getModel() { return d_model; } - /** get term database */ - quantifiers::TermDb* getTermDatabase() { return d_term_db; } - /** get term database sygus */ - quantifiers::TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; } - /** get term utilities */ - quantifiers::TermUtil* getTermUtil() { return d_term_util; } - /** get quantifiers attributes */ - quantifiers::QuantAttributes* getQuantAttributes() { - return d_quant_attr.get(); - } - /** get instantiate utility */ - quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); } - /** get skolemize utility */ - quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); } - /** get term enumeration utility */ - quantifiers::TermEnumeration* getTermEnumeration() - { - return d_term_enum.get(); - } - /** get trigger database */ - inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** notification when master equality engine is updated */ @@ -439,6 +313,117 @@ public: ~Statistics(); };/* class QuantifiersEngine::Statistics */ Statistics d_statistics; + + private: + /** reference to theory engine object */ + TheoryEngine* d_te; + /** vector of utilities for quantifiers */ + std::vector<QuantifiersUtil*> d_util; + /** vector of modules for quantifiers */ + std::vector<QuantifiersModule*> d_modules; + //------------- quantifiers utilities + /** equality query class */ + std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query; + /** equality inference class */ + std::unique_ptr<quantifiers::EqualityInference> d_eq_inference; + /** quantifiers instantiation propagtor */ + std::unique_ptr<quantifiers::InstPropagator> d_inst_prop; + /** all triggers will be stored in this trie */ + std::unique_ptr<inst::TriggerTrie> d_tr_trie; + /** extended model object */ + std::unique_ptr<quantifiers::FirstOrderModel> d_model; + /** for computing relevance of quantifiers */ + std::unique_ptr<quantifiers::QuantRelevance> d_quant_rel; + /** relevant domain */ + std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; + /** inversion utility for BV instantiation */ + std::unique_ptr<quantifiers::BvInverter> d_bv_invert; + /** model builder */ + std::unique_ptr<quantifiers::QModelBuilder> d_builder; + /** utility for effectively propositional logic */ + std::unique_ptr<quantifiers::QuantEPR> d_qepr; + /** term utilities */ + std::unique_ptr<quantifiers::TermUtil> d_term_util; + /** term database */ + std::unique_ptr<quantifiers::TermDb> d_term_db; + /** sygus term database */ + std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb; + /** quantifiers attributes */ + std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; + /** instantiate utility */ + std::unique_ptr<quantifiers::Instantiate> d_instantiate; + /** skolemize utility */ + std::unique_ptr<quantifiers::Skolemize> d_skolemize; + /** term enumeration utility */ + std::unique_ptr<quantifiers::TermEnumeration> d_term_enum; + //------------- end quantifiers utilities + //------------- quantifiers modules + /** alpha equivalence */ + std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv; + /** instantiation engine */ + std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine; + /** model engine */ + std::unique_ptr<quantifiers::ModelEngine> d_model_engine; + /** bounded integers utility */ + std::unique_ptr<quantifiers::BoundedIntegers> d_bint; + /** Conflict find mechanism for quantifiers */ + std::unique_ptr<quantifiers::QuantConflictFind> d_qcf; + /** rewrite rules utility */ + std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine; + /** subgoal generator */ + std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; + /** ceg instantiation */ + std::unique_ptr<quantifiers::CegInstantiation> d_ceg_inst; + /** lte partial instantiation */ + std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst; + /** full saturation */ + std::unique_ptr<quantifiers::InstStrategyEnum> d_fs; + /** counterexample-based quantifier instantiation */ + std::unique_ptr<quantifiers::InstStrategyCbqi> d_i_cbqi; + /** quantifiers splitting */ + std::unique_ptr<quantifiers::QuantDSplit> d_qsplit; + /** quantifiers anti-skolemization */ + std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem; + //------------- end quantifiers modules + //------------- temporary information during check + /** current effort level */ + QuantifiersModule::QEffort d_curr_effort_level; + /** are we in conflict */ + bool d_conflict; + context::CDO<bool> d_conflict_c; + /** has added lemma this round */ + bool d_hasAddedLemma; + /** whether to use model equality engine */ + bool d_useModelEe; + //------------- end temporary information during check + private: + /** list of all quantifiers seen */ + std::map<Node, bool> d_quants; + /** quantifiers pre-registered */ + NodeSet d_quants_prereg; + /** quantifiers reduced */ + BoolMap d_quants_red; + std::map<Node, Node> d_quants_red_lem; + /** list of all lemmas produced */ + // std::map< Node, bool > d_lemmas_produced; + BoolMap d_lemmas_produced_c; + /** lemmas waiting */ + std::vector<Node> d_lemmas_waiting; + /** phase requirements waiting */ + std::map<Node, bool> d_phase_req_waiting; + /** inst round counters TODO: make context-dependent? */ + context::CDO<int> d_ierCounter_c; + int d_ierCounter; + int d_ierCounter_lc; + int d_ierCounterLastLc; + int d_inst_when_phase; + /** has presolve been called */ + context::CDO<bool> d_presolve; + /** presolve cache */ + NodeSet d_presolve_in; + NodeList d_presolve_cache; + BoolList d_presolve_cache_wq; + BoolList d_presolve_cache_wic; };/* class QuantifiersEngine */ }/* CVC4::theory namespace */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ab9fa6d54..317080ba6 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -37,25 +37,28 @@ namespace sets { TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, context::Context* c, - context::UserContext* u): - d_rels(NULL), - d_members(c), - d_deq(c), - d_deq_processed(u), - d_keep(c), - d_proxy(u), - d_proxy_to_term(u), - d_lemmas_produced(u), - d_card_processed(u), - d_var_elim(u), - d_external(external), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::sets::ee", true), - d_conflict(c) + context::UserContext* u) + : d_members(c), + d_deq(c), + d_deq_processed(u), + d_keep(c), + d_sentLemma(false), + d_addedFact(false), + d_full_check_incomplete(false), + d_proxy(u), + d_proxy_to_term(u), + d_lemmas_produced(u), + d_card_enabled(false), + d_card_processed(u), + d_var_elim(u), + d_external(external), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::sets::ee", true), + d_conflict(c), + d_rels( + new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external)), + d_rels_enabled(false) { - - d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external); - d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); @@ -68,21 +71,14 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_equalityEngine.addFunctionKind(kind::MEMBER); d_equalityEngine.addFunctionKind(kind::SUBSET); - // If cardinality is on. d_equalityEngine.addFunctionKind(kind::CARD); - - d_card_enabled = false; - d_rels_enabled = false; - -}/* TheorySetsPrivate::TheorySetsPrivate() */ +} TheorySetsPrivate::~TheorySetsPrivate(){ - delete d_rels; for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) { delete current_pair.second; } -}/* TheorySetsPrivate::~TheorySetsPrivate() */ - +} void TheorySetsPrivate::eqNotifyNewClass(TNode t) { if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 31aec85c3..d36e0ddb1 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -46,8 +46,6 @@ class TheorySetsPrivate { typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; -private: - TheorySetsRels * d_rels; public: void eqNotifyNewClass(TNode t); void eqNotifyPreMerge(TNode t1, TNode t2); @@ -113,9 +111,25 @@ private: void addEqualityToExp( Node a, Node b, std::vector< Node >& exp ); void debugPrintSet( Node s, const char * c ); - + + /** sent lemma + * + * This flag is set to true during a full effort check if this theory + * called d_out->lemma(...). + */ bool d_sentLemma; + /** added fact + * + * This flag is set to true during a full effort check if this theory + * added an internal fact to its equality engine. + */ bool d_addedFact; + /** full check incomplete + * + * This flag is set to true during a full effort check if this theory + * is incomplete for some reason (for instance, if we combine cardinality + * with a relation or extended function kind). + */ bool d_full_check_incomplete; NodeMap d_proxy; NodeMap d_proxy_to_term; @@ -139,11 +153,15 @@ private: std::map< Kind, std::map< Node, std::map< Node, Node > > > d_bop_index; std::map< Kind, std::vector< Node > > d_op_list; //cardinality -private: + private: + /** is cardinality enabled? + * + * This flag is set to true during a full effort check if any constraint + * involving cardinality constraints is asserted to this theory. + */ bool d_card_enabled; /** element types of sets for which cardinality is enabled */ std::map<TypeNode, bool> d_t_card_enabled; - bool d_rels_enabled; std::map< Node, Node > d_eqc_to_card_term; NodeSet d_card_processed; std::map< Node, std::vector< Node > > d_card_parent; @@ -300,7 +318,16 @@ private: bool isCareArg( Node n, unsigned a ); public: bool isEntailed( Node n, bool pol ); - + + private: + /** subtheory solver for the theory of relations */ + std::unique_ptr<TheorySetsRels> d_rels; + /** are relations enabled? + * + * This flag is set to true during a full effort check if any constraint + * involving relational constraints is asserted to this theory. + */ + bool d_rels_enabled; };/* class TheorySetsPrivate */ diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 477e99b9b..f53f82cc4 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -34,7 +34,6 @@ RegExpOpr::RegExpOpr() std::vector<Node>{})), d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), d_one(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))), - RMAXINT(LONG_MAX), d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, std::vector<Node>{})), d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)) @@ -1137,7 +1136,8 @@ bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) { bool RegExpOpr::containC2(unsigned cnt, Node n) { if(n.getKind() == kind::REGEXP_RV) { - Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2"); + Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in RegExpOpr::containC2"); unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); return cnt == y; } else if(n.getKind() == kind::REGEXP_CONCAT) { @@ -1178,7 +1178,8 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { r1 = d_emptySingleton; r2 = d_emptySingleton; } else if(n.getKind() == kind::REGEXP_RV) { - Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::convert2"); + Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in RegExpOpr::convert2"); unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); r1 = d_emptySingleton; if(cnt == y) { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index a646f0e6f..57e68abfb 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -48,7 +48,6 @@ class RegExpOpr { Node d_emptyRegexp; Node d_zero; Node d_one; - CVC4::Rational RMAXINT; Node d_sigma; Node d_sigma_star; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ce0100686..72e82edca 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -103,7 +103,6 @@ TheoryStrings::TheoryStrings(context::Context* c, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), - RMAXINT(LONG_MAX), d_notify(*this), d_equalityEngine(d_notify, c, "theory::strings", true), d_conflict(c, false), @@ -536,7 +535,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl; if( lts[i].isConst() ) { lts_values.push_back( lts[i] ); - Assert(lts[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(lts[i].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; }else{ @@ -545,7 +545,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Node v = d_valuation.getModelValue(lts[i]); Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl; lts_values.push_back( v ); - Assert(v.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(v.getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); unsigned lvalue = v.getConst<Rational>().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; }else{ @@ -621,7 +622,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Trace("strings-model") << std::endl; //use type enumerator - Assert(lts_values[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(lts_values[i].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); for (const Node& eqc : pure_eq) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index de505f262..2c0cb42aa 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -234,7 +234,6 @@ private: Node d_zero; Node d_one; Node d_neg_one; - CVC4::Rational RMAXINT; unsigned d_card_size; // Helper functions Node getRepresentative( Node t ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 9a0fad7d8..1c68097ae 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -653,13 +653,13 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node) } TNode n1 = node[1]; NodeManager* nm = NodeManager::currentNM(); - CVC4::Rational RMAXINT(LONG_MAX); + CVC4::Rational rMaxInt(String::maxSize()); AlwaysAssert(n1.isConst(), "re.loop contains non-constant integer (1)."); AlwaysAssert(n1.getConst<Rational>().sgn() >= 0, "Negative integer in string REGEXP_LOOP (1)"); - Assert(n1.getConst<Rational>() <= RMAXINT, - "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); - unsigned l = n1.getConst<Rational>().getNumerator().toUnsignedInt(); + Assert(n1.getConst<Rational>() <= rMaxInt, + "Exceeded UINT32_MAX in string REGEXP_LOOP (1)"); + uint32_t l = n1.getConst<Rational>().getNumerator().toUnsignedInt(); std::vector<Node> vec_nodes; for (unsigned i = 0; i < l; i++) { @@ -675,9 +675,9 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node) AlwaysAssert(n2.isConst(), "re.loop contains non-constant integer (2)."); AlwaysAssert(n2.getConst<Rational>().sgn() >= 0, "Negative integer in string REGEXP_LOOP (2)"); - Assert(n2.getConst<Rational>() <= RMAXINT, - "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); - unsigned u = n2.getConst<Rational>().getNumerator().toUnsignedInt(); + Assert(n2.getConst<Rational>() <= rMaxInt, + "Exceeded UINT32_MAX in string REGEXP_LOOP (2)"); + uint32_t u = n2.getConst<Rational>().getNumerator().toUnsignedInt(); if (u <= l) { retNode = n; @@ -838,7 +838,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i } } case kind::REGEXP_LOOP: { - unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt(); + uint32_t l = r[1].getConst<Rational>().getNumerator().toUnsignedInt(); if(s.size() == index_start) { return l==0? true : testConstStringInRegExp(s, index_start, r[0]); } else if(l==0 && r[1]==r[2]) { @@ -847,7 +847,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i Assert(r.getNumChildren() == 3, "String rewriter error: LOOP has 2 children"); if(l==0) { //R{0,u} - unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); + uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); for(unsigned len=s.size() - index_start; len>=1; len--) { CVC4::String t = s.substr(index_start, len); if(testConstStringInRegExp(t, 0, r[0])) { @@ -1216,9 +1216,9 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) if (node[1].isConst() && node[2].isConst()) { CVC4::String s = node[0].getConst<String>(); - CVC4::Rational RMAXINT(LONG_MAX); - unsigned start; - if (node[1].getConst<Rational>() > RMAXINT) + CVC4::Rational rMaxInt(String::maxSize()); + uint32_t start; + if (node[1].getConst<Rational>() > rMaxInt) { // start beyond the maximum size of strings // thus, it must be beyond the end point of this string @@ -1241,7 +1241,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) return returnRewrite(node, ret, "ss-const-start-oob"); } } - if (node[2].getConst<Rational>() > RMAXINT) + if (node[2].getConst<Rational>() > rMaxInt) { // take up to the end of the string Node ret = nm->mkConst(::CVC4::String(s.suffix(s.size() - start))); @@ -1254,7 +1254,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) } else { - unsigned len = + uint32_t len = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); if (start + len > s.size()) { @@ -1743,17 +1743,17 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { getConcat(node[0], children0); if (children0[0].isConst() && node[1].isConst() && node[2].isConst()) { - CVC4::Rational RMAXINT(CVC4::String::maxSize()); - if (node[2].getConst<Rational>() > RMAXINT) + CVC4::Rational rMaxInt(CVC4::String::maxSize()); + if (node[2].getConst<Rational>() > rMaxInt) { // We know that, due to limitations on the size of string constants // in our implementation, that accessing a position greater than - // RMAXINT is guaranteed to be out of bounds. + // rMaxInt is guaranteed to be out of bounds. Node negone = nm->mkConst(Rational(-1)); return returnRewrite(node, negone, "idof-max"); } Assert(node[2].getConst<Rational>().sgn() >= 0); - unsigned start = + uint32_t start = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); CVC4::String s = children0[0].getConst<String>(); CVC4::String t = node[1].getConst<String>(); @@ -2641,10 +2641,10 @@ bool TheoryStringsRewriter::stripSymbolicLength(std::vector<Node>& n1, // we can remove part of the constant // lower bound minus the length of a concrete string is negative, // hence lowerBound cannot be larger than long max - Assert(lbr < Rational(LONG_MAX)); + Assert(lbr < Rational(String::maxSize())); curr = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::MINUS, curr, lowerBound)); - unsigned lbsize = lbr.getNumerator().toUnsignedInt(); + uint32_t lbsize = lbr.getNumerator().toUnsignedInt(); Assert(lbsize < s.size()); if (dir == 1) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c87a4be02..d75f7843d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -49,7 +49,6 @@ #include "theory/theory_model.h" #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" -#include "theory/unconstrained_simplifier.h" #include "util/resource_manager.h" using namespace std; @@ -315,7 +314,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)), d_theoryAlternatives(), d_attr_handle(), d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) @@ -360,9 +358,6 @@ TheoryEngine::~TheoryEngine() { delete d_masterEqualityEngine; smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); - - delete d_unconstrainedSimp; - smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } @@ -2146,11 +2141,6 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector }); } -void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) -{ - d_unconstrainedSimp->processAssertions(assertions); -} - void TheoryEngine::setUserAttribute(const std::string& attr, Node n, const std::vector<Node>& node_values, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 71a0234ed..65402f0a6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -99,7 +99,6 @@ namespace theory { class DecisionEngine; class RemoveTermFormulas; -class UnconstrainedSimplifier; /** * This is essentially an abstraction for a collection of theories. A @@ -827,9 +826,6 @@ private: /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); - /** For preprocessing pass simplifying unconstrained expressions */ - UnconstrainedSimplifier* d_unconstrainedSimp; - /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ public: void staticInitializeBVOptions(const std::vector<Node>& assertions); @@ -838,8 +834,6 @@ public: /** Returns false if an assertion simplified to false. */ bool donePPSimpITE(std::vector<Node>& assertions); - void ppUnconstrainedSimp(std::vector<Node>& assertions); - SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 8d68d4e86..34175a775 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -442,10 +442,8 @@ bool String::isDigit(unsigned character) return c >= '0' && c <= '9'; } -size_t String::maxSize() -{ - return std::numeric_limits<size_t>::max(); -} +size_t String::maxSize() { return std::numeric_limits<uint32_t>::max(); } + Rational String::toNumber() const { // when smt2 standard for strings is set, this may change, based on the diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 6400411cb..f707da219 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -503,6 +503,7 @@ REG0_TESTS = \ regress0/nl/magnitude-wrong-1020-m.smt2 \ regress0/nl/mult-po.smt2 \ regress0/nl/nia-wrong-tl.smt2 \ + regress0/nl/nlExtPurify-test.smt2 \ regress0/nl/nta/cos-sig-value.smt2 \ regress0/nl/nta/exp-n0.5-lb.smt2 \ regress0/nl/nta/exp-n0.5-ub.smt2 \ @@ -1301,6 +1302,7 @@ REG1_TESTS = \ regress1/quantifiers/model_6_1_bv.smt2 \ regress1/quantifiers/mutualrec2.cvc \ regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \ + regress1/quantifiers/nl-pow-trick.smt2 \ regress1/quantifiers/nra-interleave-inst.smt2 \ regress1/quantifiers/opisavailable-12.smt2 \ regress1/quantifiers/parametric-lists.smt2 \ diff --git a/test/regress/regress0/nl/nlExtPurify-test.smt2 b/test/regress/regress0/nl/nlExtPurify-test.smt2 new file mode 100644 index 000000000..1a2391c3b --- /dev/null +++ b/test/regress/regress0/nl/nlExtPurify-test.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --nl-ext-purify +; EXPECT: sat +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun skoX () Real) +(declare-fun skoS3 () Real) +(declare-fun skoSX () Real) + +(assert (and (not (<= skoX 0)) (and (not (<= (* (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX)) 0)) (not (<= skoS3 0))))) + + +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/regress1/quantifiers/nl-pow-trick.smt2 new file mode 100644 index 000000000..a369fd9f9 --- /dev/null +++ b/test/regress/regress1/quantifiers/nl-pow-trick.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --cbqi-all +; EXPECT: unsat +(set-logic NIA) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(define-fun s ((x Int)) Int (+ x 1)) +(define-fun seq ((a Int) (b Int) (k Int) (x Int)) Bool ( = x (mod (+ 1 (* b (+ 1 k))) a))) +(define-fun power ((a Int) (b Int) (c Int)) Bool +(exists ((x Int) (y Int)) (and (seq x y 0 1) (seq x y b c) (forall ((k Int) (z Int)) (=> (and (< k b) (seq x y k z)) (seq x y (+ 1 k) (* a z)))))) +) +(assert (power 2 3 8)) +(check-sat) |