summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/printer/dagification_visitor.cpp23
-rw-r--r--src/smt/smt_engine.cpp11
-rw-r--r--src/theory/evaluator.cpp566
-rw-r--r--src/theory/evaluator.h136
-rw-r--r--src/theory/quantifiers/ematching/inst_match_generator.cpp2
-rw-r--r--src/theory/quantifiers/sygus/term_database_sygus.cpp10
-rw-r--r--src/theory/quantifiers_engine.cpp2
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback