diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/dagification_visitor.cpp | 23 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 11 | ||||
-rw-r--r-- | src/theory/evaluator.cpp | 566 | ||||
-rw-r--r-- | src/theory/evaluator.h | 136 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
7 files changed, 153 insertions, 597 deletions
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index 7c0cc3101..202249759 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -46,20 +46,25 @@ DagificationVisitor::~DagificationVisitor() { } bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) { + Kind ck = current.getKind(); + if (ck == kind::FORALL || ck == kind::EXISTS || ck == kind::LAMBDA + || ck == kind::CHOICE) + { + // for quantifiers, we visit them but we don't recurse on them + visit(current, parent); + return true; + } // don't visit variables, constants, or those exprs that we've // already seen more than the threshold: if we've increased // the count beyond the threshold already, we've done the same // for all subexpressions, so it isn't useful to traverse and // increment again (they'll be dagified anyway). - return current.isVar() || - current.getMetaKind() == kind::metakind::CONSTANT || - current.getNumChildren()==0 || - ( ( current.getKind() == kind::NOT || - current.getKind() == kind::UMINUS ) && - ( current[0].isVar() || - current[0].getMetaKind() == kind::metakind::CONSTANT ) ) || - current.getKind() == kind::SORT_TYPE || - d_nodeCount[current] > d_threshold; + return current.isVar() || current.getMetaKind() == kind::metakind::CONSTANT + || current.getNumChildren() == 0 + || ((ck == kind::NOT || ck == kind::UMINUS) + && (current[0].isVar() + || current[0].getMetaKind() == kind::metakind::CONSTANT)) + || ck == kind::SORT_TYPE || d_nodeCount[current] > d_threshold; } void DagificationVisitor::visit(TNode current, TNode parent) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 22c0bcf13..331e27d95 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1656,12 +1656,13 @@ void SmtEngine::setDefaults() { } } - // by default, symmetry breaker is on only for QF_UF + // by default, symmetry breaker is on only for non-incremental QF_UF if(! options::ufSymmetryBreaker.wasSetByUser()) { - bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() - && !options::proof() && !options::unsatCores(); - Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl; - options::ufSymmetryBreaker.set(qf_uf); + bool qf_uf_noinc = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() + && !options::incrementalSolving() && !options::proof() + && !options::unsatCores(); + Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << endl; + options::ufSymmetryBreaker.set(qf_uf_noinc); } // If in arrays, set the UF handler to arrays diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 0d1536084..0d7ddbec8 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -1,499 +1,113 @@ /********************* */ -/*! \file evaluator.cpp +/*! \file evaluator.h ** \verbatim ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** 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 Evaluator class ** - ** The Evaluator class. + ** The Evaluator class can be used to evaluate terms with constant leaves + ** quickly, without going through the rewriter. **/ -#include "theory/evaluator.h" +#include "cvc4_private.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/theory.h" -#include "util/integer.h" +#ifndef __CVC4__THEORY__EVALUATOR_H +#define __CVC4__THEORY__EVALUATOR_H + +#include <utility> +#include <vector> + +#include "base/output.h" +#include "expr/node.h" +#include "util/bitvector.h" +#include "util/rational.h" +#include "util/regexp.h" namespace CVC4 { namespace theory { -Node Evaluator::eval(TNode n, - const std::vector<Node>& args, - const std::vector<Node>& vals) -{ - Trace("evaluator") << "Evaluating " << n << " under substitution " << args - << " " << vals << std::endl; - return evalInternal(n, args, vals).toNode(); -} - -EvalResult Evaluator::evalInternal(TNode n, - const std::vector<Node>& args, - const std::vector<Node>& vals) +/** + * Struct that holds the result of an evaluation. The actual value is stored in + * a union to avoid the overhead of a class hierarchy with virtual methods. + */ +struct EvalResult { - std::unordered_map<TNode, EvalResult, TNodeHashFunction> results; - std::vector<TNode> queue; - queue.emplace_back(n); - - while (queue.size() != 0) + /* Describes which type of result is being stored */ + enum { - TNode currNode = queue.back(); - - if (results.find(currNode) != results.end()) - { - queue.pop_back(); - continue; - } - - bool doEval = true; - for (const auto& currNodeChild : currNode) - { - if (results.find(currNodeChild) == results.end()) - { - queue.emplace_back(currNodeChild); - doEval = false; - } - } - - if (doEval) - { - queue.pop_back(); - - Node currNodeVal = currNode; - if (currNode.isVar()) - { - const auto& it = std::find(args.begin(), args.end(), currNode); - - if (it == args.end()) - { - return EvalResult(); - } - - ptrdiff_t pos = std::distance(args.begin(), it); - currNodeVal = vals[pos]; - } - else if (currNode.getKind() == kind::APPLY_UF - && currNode.getOperator().getKind() == kind::LAMBDA) - { - std::vector<Node> lambdaArgs(args); - std::vector<Node> lambdaVals(vals); - - Node op = currNode.getOperator(); - for (const auto& lambdaArg : op[0]) - { - lambdaArgs.insert(lambdaArgs.begin(), lambdaArg); - } - - for (const auto& lambdaVal : currNode) - { - lambdaVals.insert(lambdaVals.begin(), results[lambdaVal].toNode()); - } - - results[currNode] = evalInternal(op[1], lambdaArgs, lambdaVals); - continue; - } - - switch (currNodeVal.getKind()) - { - case kind::CONST_BOOLEAN: - results[currNode] = EvalResult(currNodeVal.getConst<bool>()); - break; - - case kind::NOT: - { - results[currNode] = EvalResult(!(results[currNode[0]].d_bool)); - break; - } - - case kind::AND: - { - bool res = results[currNode[0]].d_bool; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res && results[currNode[i]].d_bool; - } - results[currNode] = EvalResult(res); - break; - } - - case kind::OR: - { - bool res = results[currNode[0]].d_bool; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res || results[currNode[i]].d_bool; - } - results[currNode] = EvalResult(res); - break; - } - - case kind::CONST_RATIONAL: - { - const Rational& r = currNodeVal.getConst<Rational>(); - results[currNode] = EvalResult(r); - break; - } - - case kind::PLUS: - { - Rational res = results[currNode[0]].d_rat; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res + results[currNode[i]].d_rat; - } - results[currNode] = EvalResult(res); - break; - } - - case kind::MINUS: - { - const Rational& x = results[currNode[0]].d_rat; - const Rational& y = results[currNode[1]].d_rat; - results[currNode] = EvalResult(x - y); - break; - } - - case kind::MULT: - { - Rational res = results[currNode[0]].d_rat; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res * results[currNode[i]].d_rat; - } - results[currNode] = EvalResult(res); - break; - } - - case kind::GEQ: - { - const Rational& x = results[currNode[0]].d_rat; - const Rational& y = results[currNode[1]].d_rat; - results[currNode] = EvalResult(x >= y); - break; - } - - case kind::CONST_STRING: - results[currNode] = EvalResult(currNodeVal.getConst<String>()); - break; - - case kind::STRING_CONCAT: - { - String res = results[currNode[0]].d_str; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res.concat(results[currNode[i]].d_str); - } - results[currNode] = EvalResult(res); - break; - } - - case kind::STRING_LENGTH: - { - const String& s = results[currNode[0]].d_str; - results[currNode] = EvalResult(Rational(s.size())); - break; - } - - case kind::STRING_SUBSTR: - { - const String& s = results[currNode[0]].d_str; - Integer s_len(s.size()); - Integer i = results[currNode[1]].d_rat.getNumerator(); - Integer j = results[currNode[2]].d_rat.getNumerator(); - - if (i.strictlyNegative() || j.strictlyNegative() || i >= s_len) - { - results[currNode] = EvalResult(String("")); - } - else if (i + j > s_len) - { - results[currNode] = - EvalResult(s.suffix((s_len - i).toUnsignedInt())); - } - else - { - results[currNode] = - EvalResult(s.substr(i.toUnsignedInt(), j.toUnsignedInt())); - } - break; - } - - case kind::STRING_CHARAT: - { - const String& s = results[currNode[0]].d_str; - Integer s_len(s.size()); - Integer i = results[currNode[1]].d_rat.getNumerator(); - if (i.strictlyNegative() || i >= s_len) - { - results[currNode] = EvalResult(String("")); - } - else - { - results[currNode] = EvalResult(s.substr(i.toUnsignedInt(), 1)); - } - break; - } - - case kind::STRING_STRCTN: - { - const String& s = results[currNode[0]].d_str; - const String& t = results[currNode[1]].d_str; - results[currNode] = EvalResult(s.find(t) != std::string::npos); - break; - } - - case kind::STRING_STRIDOF: - { - const String& s = results[currNode[0]].d_str; - Integer s_len(s.size()); - const String& x = results[currNode[1]].d_str; - Integer i = results[currNode[2]].d_rat.getNumerator(); - - if (i.strictlyNegative() || i >= s_len) - { - results[currNode] = EvalResult(Rational(-1)); - } - else - { - size_t r = s.find(x, i.toUnsignedInt()); - if (r == std::string::npos) - { - results[currNode] = EvalResult(Rational(-1)); - } - else - { - results[currNode] = EvalResult(Rational(r)); - } - } - break; - } - - case kind::STRING_STRREPL: - { - const String& s = results[currNode[0]].d_str; - const String& x = results[currNode[1]].d_str; - const String& y = results[currNode[2]].d_str; - results[currNode] = EvalResult(s.replace(x, y)); - break; - } - - case kind::STRING_PREFIX: - { - const String& t = results[currNode[0]].d_str; - const String& s = results[currNode[1]].d_str; - if (s.size() < t.size()) - { - results[currNode] = EvalResult(false); - } - else - { - results[currNode] = EvalResult(s.prefix(t.size()) == t); - } - break; - } - - case kind::STRING_SUFFIX: - { - const String& t = results[currNode[0]].d_str; - const String& s = results[currNode[1]].d_str; - if (s.size() < t.size()) - { - results[currNode] = EvalResult(false); - } - else - { - results[currNode] = EvalResult(s.suffix(t.size()) == t); - } - break; - } - - case kind::STRING_ITOS: - { - Integer i = results[currNode[0]].d_rat.getNumerator(); - if (i.strictlyNegative()) - { - results[currNode] = EvalResult(String("")); - } - else - { - results[currNode] = EvalResult(String(i.toString())); - } - break; - } - - case kind::STRING_STOI: - { - const String& s = results[currNode[0]].d_str; - if (s.isNumber()) - { - results[currNode] = EvalResult(Rational(-1)); - } - else - { - results[currNode] = EvalResult(Rational(s.toNumber())); - } - break; - } - - case kind::CONST_BITVECTOR: - results[currNode] = EvalResult(currNodeVal.getConst<BitVector>()); - break; - - case kind::BITVECTOR_NOT: - results[currNode] = EvalResult(~results[currNode[0]].d_bv); - break; - - case kind::BITVECTOR_NEG: - results[currNode] = EvalResult(-results[currNode[0]].d_bv); - break; - - case kind::BITVECTOR_EXTRACT: - { - unsigned lo = bv::utils::getExtractLow(currNodeVal); - unsigned hi = bv::utils::getExtractHigh(currNodeVal); - results[currNode] = - EvalResult(results[currNode[0]].d_bv.extract(hi, lo)); - break; - } - - case kind::BITVECTOR_CONCAT: - { - BitVector res = results[currNode[0]].d_bv; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res.concat(results[currNode[i]].d_bv); - } - results[currNode] = EvalResult(res); - break; - } - - case kind::BITVECTOR_PLUS: - { - BitVector res = results[currNode[0]].d_bv; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res + results[currNode[i]].d_bv; - } - results[currNode] = EvalResult(res); - break; - } - - case kind::BITVECTOR_MULT: - { - BitVector res = results[currNode[0]].d_bv; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res * results[currNode[i]].d_bv; - } - results[currNode] = EvalResult(res); - break; - } - case kind::BITVECTOR_AND: - { - BitVector res = results[currNode[0]].d_bv; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res & results[currNode[i]].d_bv; - } - results[currNode] = EvalResult(res); - break; - } - - case kind::BITVECTOR_OR: - { - BitVector res = results[currNode[0]].d_bv; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res | results[currNode[i]].d_bv; - } - results[currNode] = EvalResult(res); - break; - } - - case kind::BITVECTOR_XOR: - { - BitVector res = results[currNode[0]].d_bv; - for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) - { - res = res ^ results[currNode[i]].d_bv; - } - results[currNode] = EvalResult(res); - break; - } - - case kind::EQUAL: - { - EvalResult lhs = results[currNode[0]]; - EvalResult rhs = results[currNode[1]]; - - switch (lhs.d_tag) - { - case EvalResult::BOOL: - { - results[currNode] = EvalResult(lhs.d_bool == rhs.d_bool); - break; - } - - case EvalResult::BITVECTOR: - { - results[currNode] = EvalResult(lhs.d_bv == rhs.d_bv); - break; - } - - case EvalResult::RATIONAL: - { - results[currNode] = EvalResult(lhs.d_rat == rhs.d_rat); - break; - } - - case EvalResult::STRING: - { - results[currNode] = EvalResult(lhs.d_str == rhs.d_str); - break; - } - - default: - { - Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0]) - << " not supported" << std::endl; - return EvalResult(); - break; - } - } - - break; - } - - case kind::ITE: - { - if (results[currNode[0]].d_bool) - { - results[currNode] = results[currNode[1]]; - } - else - { - results[currNode] = results[currNode[2]]; - } - break; - } - - default: - { - Trace("evaluator") << "Kind " << currNodeVal.getKind() - << " not supported" << std::endl; - return EvalResult(); - } - } - } - } - - return results[n]; -} + BOOL, + BITVECTOR, + RATIONAL, + STRING, + INVALID + } d_tag; + + /* Stores the actual result */ + union + { + bool d_bool; + BitVector d_bv; + Rational d_rat; + String d_str; + }; + + EvalResult(const EvalResult& other); + EvalResult() : d_tag(INVALID) {} + EvalResult(bool b) : d_tag(BOOL), d_bool(b) {} + EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {} + EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {} + EvalResult(const String& str) : d_tag(STRING), d_str(str) {} + + EvalResult& operator=(const EvalResult& other); + + ~EvalResult(); + + /** + * Converts the result to a Node. If the result is not valid, this function + * returns the null node. + */ + Node toNode() const; +}; + +/** + * The class that performs the actual evaluation of a term under a + * substitution. Right now, the class does not cache anything between different + * calls to `eval` but this might change in the future. + */ +class Evaluator +{ + public: + /** + * Evaluates node `n` under the substitution described by the variable names + * `args` and the corresponding values `vals`. The function returns a null + * node if there is a subterm that is not constant under the substitution or + * if an operator is not supported by the evaluator. + */ + Node eval(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals); + + private: + /** + * Evaluates node `n` under the substitution described by the variable names + * `args` and the corresponding values `vals`. The internal version returns + * an EvalResult which has slightly less overhead for recursive calls. The + * function returns an invalid result if there is a subterm that is not + * constant under the substitution or if an operator is not supported by the + * evaluator. + */ + EvalResult evalInternal(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals); +}; } // namespace theory } // namespace CVC4 + +#endif /* __CVC4__THEORY__EVALUATOR_H */ diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index cee8a0d21..0d7ddbec8 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -4,19 +4,21 @@ ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** 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 Evaluator class ** - ** The Evaluator class. + ** The Evaluator class can be used to evaluate terms with constant leaves + ** quickly, without going through the rewriter. **/ #include "cvc4_private.h" -#pragma once +#ifndef __CVC4__THEORY__EVALUATOR_H +#define __CVC4__THEORY__EVALUATOR_H #include <utility> #include <vector> @@ -30,8 +32,13 @@ namespace CVC4 { namespace theory { +/** + * Struct that holds the result of an evaluation. The actual value is stored in + * a union to avoid the overhead of a class hierarchy with virtual methods. + */ struct EvalResult { + /* Describes which type of result is being stored */ enum { BOOL, @@ -41,6 +48,7 @@ struct EvalResult INVALID } d_tag; + /* Stores the actual result */ union { bool d_bool; @@ -49,117 +57,51 @@ struct EvalResult String d_str; }; - EvalResult(const EvalResult& other) - { - d_tag = other.d_tag; - switch (d_tag) - { - case BOOL: d_bool = other.d_bool; break; - case BITVECTOR: - new (&d_bv) BitVector; - d_bv = other.d_bv; - break; - case RATIONAL: - new (&d_rat) Rational; - d_rat = other.d_rat; - break; - case STRING: - new (&d_str) String; - d_str = other.d_str; - break; - case INVALID: break; - } - } - + EvalResult(const EvalResult& other); EvalResult() : d_tag(INVALID) {} - EvalResult(bool b) : d_tag(BOOL), d_bool(b) {} - EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {} - EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {} - EvalResult(const String& str) : d_tag(STRING), d_str(str) {} - EvalResult& operator=(const EvalResult& other) - { - if (this != &other) - { - d_tag = other.d_tag; - switch (d_tag) - { - case BOOL: d_bool = other.d_bool; break; - case BITVECTOR: - new (&d_bv) BitVector; - d_bv = other.d_bv; - break; - case RATIONAL: - new (&d_rat) Rational; - d_rat = other.d_rat; - break; - case STRING: - new (&d_str) String; - d_str = other.d_str; - break; - case INVALID: break; - } - } - return *this; - } - - ~EvalResult() - { - switch (d_tag) - { - case BITVECTOR: - { - d_bv.~BitVector(); - break; - } - case RATIONAL: - { - d_rat.~Rational(); - break; - } - case STRING: - { - d_str.~String(); - break; + EvalResult& operator=(const EvalResult& other); - default: break; - } - } - } + ~EvalResult(); - Node toNode() - { - NodeManager* nm = NodeManager::currentNM(); - switch (d_tag) - { - case EvalResult::BOOL: return nm->mkConst(d_bool); - case EvalResult::BITVECTOR: return nm->mkConst(d_bv); - case EvalResult::RATIONAL: return nm->mkConst(d_rat); - case EvalResult::STRING: return nm->mkConst(d_str); - default: - { - Trace("evaluator") << "Missing conversion from " << d_tag << " to node" - << std::endl; - return Node(); - } - } - - return Node(); - } + /** + * Converts the result to a Node. If the result is not valid, this function + * returns the null node. + */ + Node toNode() const; }; +/** + * The class that performs the actual evaluation of a term under a + * substitution. Right now, the class does not cache anything between different + * calls to `eval` but this might change in the future. + */ class Evaluator { public: + /** + * Evaluates node `n` under the substitution described by the variable names + * `args` and the corresponding values `vals`. The function returns a null + * node if there is a subterm that is not constant under the substitution or + * if an operator is not supported by the evaluator. + */ Node eval(TNode n, const std::vector<Node>& args, const std::vector<Node>& vals); private: + /** + * Evaluates node `n` under the substitution described by the variable names + * `args` and the corresponding values `vals`. The internal version returns + * an EvalResult which has slightly less overhead for recursive calls. The + * function returns an invalid result if there is a subterm that is not + * constant under the substitution or if an operator is not supported by the + * evaluator. + */ EvalResult evalInternal(TNode n, const std::vector<Node>& args, const std::vector<Node>& vals); @@ -167,3 +109,5 @@ class Evaluator } // namespace theory } // namespace CVC4 + +#endif /* __CVC4__THEORY__EVALUATOR_H */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 6fd9ae418..90d1815a4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -421,7 +421,7 @@ int InstMatchGenerator::getNextMatch(Node f, Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl; success = getMatch(f, t, m, qe, tparent); if( d_independent_gen && success<0 ){ - Assert( d_eq_class.isNull() ); + Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull()); d_curr_exclude_match[t] = true; } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index a6b2b617c..5e2187e7a 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -24,6 +24,8 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "options/base_options.h" +#include "printer/printer.h" using namespace CVC4::kind; @@ -1761,14 +1763,6 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, } if (!res.isNull()) { - /* - std::cout << bn << std::endl; - std::cout << res << std::endl; - std::cout << Rewriter::rewrite(bn.substitute(it->second.begin(), - it->second.end(), - args.begin(), - args.end())) << std::endl; - */ Assert(res == Rewriter::rewrite(bn.substitute(it->second.begin(), it->second.end(), diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1fa3514c8..37f11f9cd 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -799,8 +799,6 @@ void QuantifiersEngine::registerQuantifierInternal(Node f) // this call Assert(d_lemmas_waiting.size() == prev_lemma_waiting); } - // TODO (#2020): remove this - Node ceBody = d_term_util->getInstConstantBody(f); Trace("quant-debug") << "...finish." << std::endl; d_quants[f] = true; AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting); |