Towards improving coverage.
return out;
}
-/* output stream insertion operator for benchmark statuses */
-std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
-{
- switch (status)
- {
- case SMT_SATISFIABLE: return out << "sat";
-
- case SMT_UNSATISFIABLE: return out << "unsat";
-
- case SMT_UNKNOWN: return out << "unknown";
-
- default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
- }
-}
-
/* -------------------------------------------------------------------------- */
/* class CommandPrintSuccess */
/* -------------------------------------------------------------------------- */
std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC5_EXPORT;
std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC5_EXPORT;
-/** The status an SMT benchmark can have */
-enum BenchmarkStatus
-{
- /** Benchmark is satisfiable */
- SMT_SATISFIABLE,
- /** Benchmark is unsatisfiable */
- SMT_UNSATISFIABLE,
- /** The status of the benchmark is unknown */
- SMT_UNKNOWN
-}; /* enum BenchmarkStatus */
-
-std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC5_EXPORT;
-
/**
* IOStream manipulator to print success messages or not.
*
return Constant(nm->mkConstRealOrInt(rat));
}
-size_t Variable::getComplexity() const{
- return 1u;
-}
-
-size_t VarList::getComplexity() const{
- if(empty()){
- return 1;
- }else if(singleton()){
- return 1;
- }else{
- return size() + 1;
- }
-}
-
-size_t Monomial::getComplexity() const{
- return getConstant().getComplexity() + getVarList().getComplexity();
-}
-
-size_t Polynomial::getComplexity() const{
- size_t cmp = 0;
- iterator i = begin(), e = end();
- for(; i != e; ++i){
- Monomial m = *i;
- cmp += m.getComplexity();
- }
- return cmp;
-}
-
-size_t Constant::getComplexity() const{
- return getValue().complexity();
-}
-
bool Variable::isLeafMember(Node n){
return (!isRelationOperator(n.getKind())) &&
(Theory::isLeafOf(n, theory::THEORY_ARITH));
return k == kind::CONST_RATIONAL || k == kind::CONST_INTEGER;
}
-size_t Comparison::getComplexity() const{
- switch(comparisonKind()){
- case kind::CONST_BOOLEAN: return 1;
- case kind::LT:
- case kind::LEQ:
- case kind::DISTINCT:
- case kind::EQUAL:
- case kind::GT:
- case kind::GEQ:
- return getLeft().getComplexity() + getRight().getComplexity();
- default: Unhandled() << comparisonKind(); return -1;
- }
-}
-
Polynomial Comparison::getLeft() const {
TNode left;
Kind k = comparisonKind();
bool operator==(const Variable& v) const { return getNode() == v.getNode();}
- size_t getComplexity() const;
};/* class Variable */
class Constant : public NodeWrapper {
return getValue().getNumerator().length();
}
- size_t getComplexity() const;
-
};/* class Constant */
}
return true;
}
- size_t getComplexity() const;
private:
bool isSorted(iterator start, iterator end);
void print() const;
static void printList(const std::vector<Monomial>& list);
- size_t getComplexity() const;
};/* class Monomial */
class SumPair;
return getHead().getVarList();
}
- size_t getComplexity() const;
-
friend class SumPair;
friend class Comparison;
return parse.isNormalForm();
}
- size_t getComplexity() const;
-
SumPair toSumPair() const;
Polynomial normalizedVariablePart() const;
uint64_t& addedLemmas)
{
// see if these produce new matches
- d_children_trie[fromChildIndex].addInstMatch(d_qstate, d_quant, m.get());
+ d_children_trie[fromChildIndex].addInstMatch(d_quant, m.get());
// possibly only do the following if we know that new matches will be
// produced? the issue is that instantiations are filtered in quantifiers
// engine, and so there is no guarentee that
}
InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
-size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
-{
- std::map<Node, std::vector<Trigger*> >::const_iterator it =
- d_user_gen.find(q);
- if (it == d_user_gen.end())
- {
- return 0;
- }
- return it->second.size();
-}
-
-Trigger* InstStrategyUserPatterns::getUserGenerator(Node q, size_t i) const
-{
- std::map<Node, std::vector<Trigger*> >::const_iterator it =
- d_user_gen.find(q);
- if (it == d_user_gen.end())
- {
- return nullptr;
- }
- Assert(i < it->second.size());
- return it->second[i];
-}
-
std::string InstStrategyUserPatterns::identify() const
{
return std::string("UserPatterns");
~InstStrategyUserPatterns();
/** add pattern */
void addUserPattern(Node q, Node pat);
- /** get num patterns */
- size_t getNumUserGenerators(Node q) const;
- /** get user pattern */
- inst::Trigger* getUserGenerator(Node q, size_t i) const;
/** identify */
std::string identify() const override;
#include "theory/quantifiers/inst_match_trie.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/uf/equality_engine_iterator.h"
-
using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
namespace quantifiers {
-bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
- Node q,
+bool InstMatchTrie::existsInstMatch(Node q,
const std::vector<Node>& m,
- bool modEq,
ImtIndexOrder* imtio,
unsigned index)
{
- return !addInstMatch(qs, q, m, modEq, imtio, true, index);
+ return !addInstMatch(q, m, imtio, true, index);
}
-bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
- Node f,
+bool InstMatchTrie::addInstMatch(Node f,
const std::vector<Node>& m,
- bool modEq,
ImtIndexOrder* imtio,
bool onlyExist,
unsigned index)
std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
if (it != d_data.end())
{
- bool ret =
- it->second.addInstMatch(qs, f, m, modEq, imtio, onlyExist, index + 1);
+ bool ret = it->second.addInstMatch(f, m, imtio, onlyExist, index + 1);
if (!onlyExist || !ret)
{
return ret;
}
}
- if (modEq)
- {
- // check modulo equality if any other instantiation match exists
- if (!n.isNull() && qs.hasTerm(n))
- {
- eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
- while (!eqc.isFinished())
- {
- Node en = (*eqc);
- if (en != n)
- {
- std::map<Node, InstMatchTrie>::iterator itc = d_data.find(en);
- if (itc != d_data.end())
- {
- if (itc->second.addInstMatch(
- qs, f, m, modEq, imtio, true, index + 1))
- {
- return false;
- }
- }
- }
- ++eqc;
- }
- }
- }
if (!onlyExist)
{
- d_data[n].addInstMatch(qs, f, m, modEq, imtio, false, index + 1);
+ d_data[n].addInstMatch(f, m, imtio, false, index + 1);
}
return true;
}
}
bool CDInstMatchTrie::existsInstMatch(context::Context* context,
- quantifiers::QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
- bool modEq,
unsigned index)
{
- return !addInstMatch(context, qs, q, m, modEq, index, true);
+ return !addInstMatch(context, q, m, index, true);
}
bool CDInstMatchTrie::addInstMatch(context::Context* context,
- quantifiers::QuantifiersState& qs,
Node f,
const std::vector<Node>& m,
- bool modEq,
unsigned index,
bool onlyExist)
{
std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
if (it != d_data.end())
{
- bool ret =
- it->second->addInstMatch(context, qs, f, m, modEq, index + 1, onlyExist);
+ bool ret = it->second->addInstMatch(context, f, m, index + 1, onlyExist);
if (!onlyExist || !ret)
{
return reset || ret;
}
}
- if (modEq)
- {
- // check modulo equality if any other instantiation match exists
- if (!n.isNull() && qs.hasTerm(n))
- {
- eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
- while (!eqc.isFinished())
- {
- Node en = (*eqc);
- if (en != n)
- {
- std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
- if (itc != d_data.end())
- {
- if (itc->second->addInstMatch(
- context, qs, f, m, modEq, index + 1, true))
- {
- return false;
- }
- }
- }
- ++eqc;
- }
- }
- }
-
if (!onlyExist)
{
CDInstMatchTrie* imt = new CDInstMatchTrie(context);
Assert(d_data.find(n) == d_data.end());
d_data[n] = imt;
- imt->addInstMatch(context, qs, f, m, modEq, index + 1, false);
+ imt->addInstMatch(context, f, m, index + 1, false);
}
return true;
}
print(out, q, terms);
}
-bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs,
- Node q,
- const std::vector<Node>& m,
- bool modEq)
+bool InstMatchTrieOrdered::addInstMatch(Node q, const std::vector<Node>& m)
{
- return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
+ return d_imt.addInstMatch(q, m, d_imtio);
}
-bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
- Node q,
- const std::vector<Node>& m,
- bool modEq)
+bool InstMatchTrieOrdered::existsInstMatch(Node q, const std::vector<Node>& m)
{
- return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
+ return d_imt.existsInstMatch(q, m, d_imtio);
}
} // namespace quantifiers
* This method considers the entry given by m, starting at the given index.
* The domain of m is the bound variables of quantified formula q.
* It returns true if (the suffix) of m exists in this trie.
- * If modEq is true, we check for duplication modulo equality the current
- * equalities in the equality engine of qs.
*/
- bool existsInstMatch(QuantifiersState& qs,
- Node q,
+ bool existsInstMatch(Node q,
const std::vector<Node>& m,
- bool modEq = false,
ImtIndexOrder* imtio = nullptr,
unsigned index = 0);
/** add inst match
* This method adds (the suffix of) m starting at the given index to this
* trie, and returns true if and only if m did not already occur in this trie.
* The domain of m is the bound variables of quantified formula q.
- * If modEq is true, we check for duplication modulo equality the current
- * equalities in the equality engine of qs.
*/
- bool addInstMatch(QuantifiersState& qs,
- Node f,
+ bool addInstMatch(Node f,
const std::vector<Node>& m,
- bool modEq = false,
ImtIndexOrder* imtio = nullptr,
bool onlyExist = false,
unsigned index = 0);
* This method considers the entry given by m, starting at the given index.
* The domain of m is the bound variables of quantified formula q.
* It returns true if (the suffix) of m exists in this trie.
- * If modEq is true, we check for duplication modulo equality the current
- * equalities in the equality engine of qs.
* It additionally takes a context c, for which the entry is valid in.
*/
bool existsInstMatch(context::Context* context,
- QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
- bool modEq = false,
unsigned index = 0);
/** add inst match
*
* This method adds (the suffix of) m starting at the given index to this
* trie, and returns true if and only if m did not already occur in this trie.
* The domain of m is the bound variables of quantified formula q.
- * If modEq is true, we check for duplication modulo equality the current
- * equalities in the equality engine of qs.
* It additionally takes a context c, for which the entry is valid in.
*/
bool addInstMatch(context::Context* context,
- QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
- bool modEq = false,
unsigned index = 0,
bool onlyExist = false);
/** remove inst match
/** add match m for quantified formula q
*
* This method returns true if the match m was not previously added to this
- * class. If modEq is true, we consider duplicates modulo the current
- * equalities stored in the equality engine of qs.
+ * class.
*/
- bool addInstMatch(QuantifiersState& qs,
- Node q,
- const std::vector<Node>& m,
- bool modEq = false);
+ bool addInstMatch(Node q, const std::vector<Node>& m);
/** returns true if this trie contains m
*
* This method returns true if the match m exists in this
- * class. If modEq is true, we consider duplicates modulo the current
- * equalities stored in the equality engine of qs.
+ * class.
*/
- bool existsInstMatch(QuantifiersState& qs,
- Node q,
- const std::vector<Node>& m,
- bool modEq = false);
+ bool existsInstMatch(Node q, const std::vector<Node>& m);
private:
/** the ordering */
d_recordedInst[q].push_back(inst);
}
-bool Instantiate::existsInstantiation(Node q,
- const std::vector<Node>& terms,
- bool modEq)
+bool Instantiate::existsInstantiation(Node q, const std::vector<Node>& terms)
{
if (options().base.incrementalSolving)
{
std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
if (it != d_c_inst_match_trie.end())
{
- return it->second->existsInstMatch(userContext(), d_qstate, q, terms, modEq);
+ return it->second->existsInstMatch(userContext(), q, terms);
}
}
else
std::map<Node, InstMatchTrie>::iterator it = d_inst_match_trie.find(q);
if (it != d_inst_match_trie.end())
{
- return it->second.existsInstMatch(d_qstate, q, terms, modEq);
+ return it->second.existsInstMatch(q, terms);
}
}
return false;
res.first->second = new CDInstMatchTrie(userContext());
}
d_c_inst_match_trie_dom.insert(q);
- return res.first->second->addInstMatch(userContext(), d_qstate, q, terms);
+ return res.first->second->addInstMatch(userContext(), q, terms);
}
Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
- return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms);
+ return d_inst_match_trie[q].addInstMatch(q, terms);
}
bool Instantiate::removeInstantiationInternal(Node q,
*
* Returns true if and only if the instantiation already was added or
* recorded by this class.
- * modEq : whether to check for duplication modulo equality
*/
- bool existsInstantiation(Node q,
- const std::vector<Node>& terms,
- bool modEq = false);
+ bool existsInstantiation(Node q, const std::vector<Node>& terms);
//--------------------------------------general utilities
/** get instantiation
*
#include "theory/quantifiers/quantifiers_state.h"
#include "options/quantifiers_options.h"
+#include "theory/uf/equality_engine.h"
#include "theory/uf/equality_engine_iterator.h"
namespace cvc5::internal {
std::map<TypeNode, uint64_t> tnum;
while (!eqcs_i.isFinished())
{
- TNode r = (*eqcs_i);
- TypeNode tr = r.getType();
- if (tnum.find(tr) == tnum.end())
- {
- tnum[tr] = 0;
- }
- tnum[tr]++;
- bool firstTime = true;
- Trace(c) << " " << r;
- Trace(c) << " : { ";
- eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
- while (!eqc_i.isFinished())
- {
- TNode n = (*eqc_i);
- if (r != n)
- {
- if (firstTime)
- {
- Trace(c) << std::endl;
- firstTime = false;
- }
- Trace(c) << " " << n << std::endl;
- }
- ++eqc_i;
- }
- if (!firstTime)
- {
- Trace(c) << " ";
- }
- Trace(c) << "}" << std::endl;
+ tnum[(*eqcs_i).getType()]++;
++eqcs_i;
}
- Trace(c) << std::endl;
+ Trace(c) << ee->debugPrintEqc() << std::endl;
for (const std::pair<const TypeNode, uint64_t>& t : tnum)
{
Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl;
return false;
}
-/******************** Model generation ********************/
-/******************** Model generation ********************/
-/******************** Model generation ********************/
-
-namespace {
-/**
- * This function is a helper function to print sets as
- * Set A = { a0, a1, a2, }
- * instead of
- * (union (singleton a0) (union (singleton a1) (singleton a2)))
- */
-void traceSetElementsRecursively(stringstream& stream, const Node& set)
-{
- Assert(set.getType().isSet());
- if (set.getKind() == SET_SINGLETON)
- {
- stream << set[0] << ", ";
- }
- if (set.getKind() == SET_UNION)
- {
- traceSetElementsRecursively(stream, set[0]);
- traceSetElementsRecursively(stream, set[1]);
- }
-}
-
-std::string traceElements(const Node& set)
-{
- std::stringstream stream;
- traceSetElementsRecursively(stream, set);
- return stream.str();
-}
-
-} // namespace
-
bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
const std::set<Node>& termSet)
{
m->assertSkeleton(el);
}
- Trace("sets-model") << "Set " << eqc << " = { " << traceElements(rep)
- << " }" << std::endl;
+ Trace("sets-model") << "Set " << eqc << " = " << els << std::endl;
}
}
Node UfModelTreeNode::getFunctionValue(const std::vector<Node>& args,
int index,
- Node argDefaultValue,
- bool simplify)
+ Node argDefaultValue)
{
if(!d_data.empty()) {
Node defaultValue = argDefaultValue;
if(d_data.find(Node::null()) != d_data.end()) {
- defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify);
+ defaultValue = d_data[Node::null()].getFunctionValue(
+ args, index + 1, argDefaultValue);
}
std::vector<Node> caseArgs;
{
if (!p.first.isNull())
{
- Node val =
- p.second.getFunctionValue(args, index + 1, defaultValue, simplify);
+ Node val = p.second.getFunctionValue(args, index + 1, defaultValue);
caseArgs.push_back(p.first);
caseValues[p.first] = val;
}
NodeManager* nm = NodeManager::currentNM();
Node retNode = defaultValue;
-
- if(!simplify) {
- // "non-simplifying" mode - expand function values to things like:
- // IF (x=0 AND y=0 AND z=0) THEN value1
- // ELSE IF (x=0 AND y=0 AND z=1) THEN value2
- // [...etc...]
- for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
- Node val = caseValues[ caseArgs[ i ] ];
- if(val.getKind() == ITE) {
- // use a stack to reverse the order, since we're traversing outside-in
- std::stack<TNode> stk;
- do {
- stk.push(val);
- val = val[2];
- } while(val.getKind() == ITE);
- AlwaysAssert(val == defaultValue)
- << "default values don't match when constructing function "
- "definition!";
- while(!stk.empty()) {
- val = stk.top();
- stk.pop();
- retNode = nm->mkNode(ITE, nm->mkNode(AND, args[index].eqNode(caseArgs[i]), val[0]), val[1], retNode);
- }
- } else {
- retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
- }
- }
- } else {
- // "simplifying" mode - condense function values
- for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
- retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
- }
+ // condense function values
+ for (size_t i = 0, cargs = caseArgs.size(); i < cargs; i++)
+ {
+ size_t ii = cargs - i - 1;
+ retNode = nm->mkNode(ITE,
+ args[index].eqNode(caseArgs[ii]),
+ caseValues[caseArgs[ii]],
+ retNode);
}
return retNode;
- } else {
- Assert(!d_value.isNull());
- return d_value;
}
+ Assert(!d_value.isNull());
+ return d_value;
}
//update function
Node UfModelTree::getFunctionValue(const std::vector<Node>& args, Rewriter* r)
{
- Node body = d_tree.getFunctionValue(args, 0, Node::null(), r != nullptr);
+ Node body = d_tree.getFunctionValue(args, 0, Node::null());
if (r != nullptr)
{
body = r->rewrite(body);
/** getFunctionValue */
Node getFunctionValue(const std::vector<Node>& args,
int index,
- Node argDefaultValue,
- bool simplify = true);
+ Node argDefaultValue);
/** update function */
void update( TheoryModel* m );
/** simplify function */
projects / cvc5.git / commitdiff