theory/arrays/theory_arrays_type_rules.h
theory/arrays/type_enumerator.h
theory/arrays/type_enumerator.cpp
- theory/arrays/union_find.cpp
- theory/arrays/union_find.h
theory/assertion.cpp
theory/assertion.h
theory/atom_requests.cpp
void TheoryArithPrivate::outputRestart() {
Trace("arith::channel") << "Arith restart!" << std::endl;
- (d_containing.d_out)->demandRestart();
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ Node restartVar = sm->mkDummySkolem(
+ "restartVar",
+ nm->booleanType(),
+ "A boolean variable asserted to be true to force a restart");
+ d_containing.d_im.lemma(
+ restartVar, InferenceId::ARITH_DEMAND_RESTART, LemmaProperty::REMOVABLE);
}
bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool emmmittedLemmaOrSplit){
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 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.
- * ****************************************************************************
- *
- * Path-compressing, backtrackable union-find using an undo
- * stack. Refactored from the UF union-find.
- */
-
-#include <iostream>
-
-#include "expr/node.h"
-#include "theory/arrays/union_find.h"
-
-using namespace std;
-
-namespace cvc5::internal {
-namespace theory {
-namespace arrays {
-
-template <class NodeType, class NodeHash>
-void UnionFind<NodeType, NodeHash>::notify() {
- Trace("arraysuf") << "arraysUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl;
- while(d_offset < d_trace.size()) {
- pair<TNode, TNode> p = d_trace.back();
- if(p.second.isNull()) {
- d_map.erase(p.first);
- Trace("arraysuf") << "arraysUF " << d_trace.size() << " erasing " << p.first << endl;
- } else {
- d_map[p.first] = p.second;
- Trace("arraysuf") << "arraysUF " << d_trace.size() << " replacing " << p << endl;
- }
- d_trace.pop_back();
- }
- Trace("arraysuf") << "arraysUF cancelling finished." << endl;
-}
-
-// The following declarations allow us to put functions in the .cpp file
-// instead of the header, since we know which instantiations are needed.
-
-template void UnionFind<Node, std::hash<Node>>::notify();
-
-template void UnionFind<TNode, std::hash<TNode>>::notify();
-
-} // namespace arrays
-} // namespace theory
-} // namespace cvc5::internal
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Mathias Preiner, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 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.
- * ****************************************************************************
- *
- * Path-compressing, backtrackable union-find using an undo
- * stack. Refactored from the UF union-find.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__THEORY__ARRAYS__UNION_FIND_H
-#define CVC5__THEORY__ARRAYS__UNION_FIND_H
-
-#include <utility>
-#include <vector>
-#include <unordered_map>
-
-#include "expr/node.h"
-#include "context/cdo.h"
-
-namespace cvc5::context {
-class Context;
-}
-
-namespace cvc5::internal {
-namespace theory {
-namespace arrays {
-
-// NodeType \in { Node, TNode }
-template <class NodeType, class NodeHash>
-class UnionFind : context::ContextNotifyObj
-{
- /** Our underlying map type. */
- typedef std::unordered_map<NodeType, NodeType, NodeHash> MapType;
-
- /**
- * Our map of Nodes to their canonical representatives.
- * If a Node is not present in the map, it is its own
- * representative.
- */
- MapType d_map;
-
- /** Our undo stack for changes made to d_map. */
- std::vector<std::pair<TNode, TNode> > d_trace;
-
- /** Our current offset in the d_trace stack (context-dependent). */
- context::CDO<size_t> d_offset;
-
- public:
- UnionFind(context::Context* ctxt)
- : context::ContextNotifyObj(ctxt), d_offset(ctxt, 0)
- {
- }
-
- /**
- * Return a Node's union-find representative, doing path compression.
- */
- inline TNode find(TNode n);
-
- /**
- * Return a Node's union-find representative, NOT doing path compression.
- * This is useful for Assert() statements, debug checking, and similar
- * things that you do NOT want to mutate the structure.
- */
- inline TNode debugFind(TNode n) const;
-
- /**
- * Set the canonical representative of n to newParent. They should BOTH
- * be their own canonical representatives on entry to this funciton.
- */
- inline void setCanon(TNode n, TNode newParent);
-
- /**
- * Called by the Context when a pop occurs. Cancels everything to the
- * current context level. Overrides ContextNotifyObj::notify().
- */
- void notify();
-
-}; /* class UnionFind<> */
-
-template <class NodeType, class NodeHash>
-inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
- typename MapType::const_iterator i = d_map.find(n);
- if(i == d_map.end()) {
- return n;
- } else {
- return debugFind((*i).second);
- }
-}
-
-template <class NodeType, class NodeHash>
-inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) {
- Trace("arraysuf") << "arraysUF find of " << n << std::endl;
- typename MapType::iterator i = d_map.find(n);
- if(i == d_map.end()) {
- Trace("arraysuf") << "arraysUF it is rep" << std::endl;
- return n;
- } else {
- Trace("arraysuf") << "arraysUF not rep: par is " << (*i).second << std::endl;
- std::pair<TNode, TNode> pr = *i;
- // our iterator is invalidated by the recursive call to find(),
- // since it mutates the map
- TNode p = find(pr.second);
- if(p == pr.second) {
- return p;
- }
- d_trace.push_back(std::make_pair(n, pr.second));
- d_offset = d_trace.size();
- Trace("arraysuf") << "arraysUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl;
- pr.second = p;
- d_map.insert(pr);
- return p;
- }
-}
-
-template <class NodeType, class NodeHash>
-inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
- Assert(d_map.find(n) == d_map.end());
- Assert(d_map.find(newParent) == d_map.end());
- if(n != newParent) {
- Trace("arraysuf") << "arraysUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl;
- d_map[n] = newParent;
- d_trace.push_back(std::make_pair(n, TNode::null()));
- d_offset = d_trace.size();
- }
-}
-
-} // namespace arrays
-} // namespace theory
-} // namespace cvc5::internal
-
-#endif /*CVC5__THEORY__ARRAYS__UNION_FIND_H */
+ "lemmas")),
requirePhase(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+ "requirePhase")),
- restartDemands(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
- + "restartDemands")),
trustedConflicts(smtStatisticsRegistry().registerInt(
getStatsPrefix(theory) + "trustedConflicts")),
trustedLemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
d_engine->conflict(tConf, d_theory);
}
-void EngineOutputChannel::demandRestart()
-{
- NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- Node restartVar = sm->mkDummySkolem(
- "restartVar",
- nm->booleanType(),
- "A boolean variable asserted to be true to force a restart");
- Trace("theory::restart") << "EngineOutputChannel<" << d_theory
- << ">::restart(" << restartVar << ")" << std::endl;
- ++d_statistics.restartDemands;
- lemma(restartVar, LemmaProperty::REMOVABLE);
-}
-
void EngineOutputChannel::requirePhase(TNode n, bool phase)
{
Trace("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
void lemma(TNode lemma, LemmaProperty p = LemmaProperty::NONE) override;
- void demandRestart() override;
-
void requirePhase(TNode n, bool phase) override;
void setIncomplete(IncompleteId id) override;
{
public:
Statistics(theory::TheoryId theory);
- /** Number of calls to conflict, propagate, lemma, requirePhase,
- * restartDemands */
- IntStat conflicts, propagations, lemmas, requirePhase, restartDemands,
- trustedConflicts, trustedLemmas;
+ /** Number of calls to conflict, propagate, lemma, requirePhase */
+ IntStat conflicts, propagations, lemmas, requirePhase, trustedConflicts,
+ trustedLemmas;
};
/** The theory engine we're communicating with. */
TheoryEngine* d_engine;
case InferenceId::ARITH_ROW_IMPL: return "ARITH_ROW_IMPL";
case InferenceId::ARITH_SPLIT_FOR_NL_MODEL:
return "ARITH_SPLIT_FOR_NL_MODEL";
+ case InferenceId::ARITH_DEMAND_RESTART: return "ARITH_DEMAND_RESTART";
case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA:
return "ARITH_PP_ELIM_OPERATORS_LEMMA";
// variables in a model, but those variables are inconsistent with assignments
// from another theory
ARITH_SPLIT_FOR_NL_MODEL,
+ // dummy lemma to demand a restart
+ ARITH_DEMAND_RESTART,
//-------------------- preprocessing
// equivalence of term and its preprocessed form
ARITH_PP_ELIM_OPERATORS,
*/
virtual void handleUserAttribute(const char* attr, Theory* t) {}
- /** Demands that the search restart from sat search level 0.
- * Using this leads to non-termination issues.
- * It is appropriate for prototyping for theories.
- */
- virtual void demandRestart() {}
-
//---------------------------- new proof
/**
* Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
InstantiationEngine::~InstantiationEngine() {}
+std::string InstantiationEngine::identify() const { return "InstEngine"; }
+
void InstantiationEngine::presolve() {
for( unsigned i=0; i<d_instStrategies.size(); ++i ){
d_instStrategies[i]->presolve();
bool checkCompleteFor(Node q) override;
void checkOwnership(Node q) override;
void registerQuantifier(Node q) override;
- Node explain(TNode n) { return Node::null(); }
/** add user pattern */
void addUserPattern(Node q, Node pat);
void addUserNoPattern(Node q, Node pat);
/** Identify this module */
- std::string identify() const override { return "InstEngine"; }
+ std::string identify() const override;
private:
- /** is the engine incomplete for this quantifier */
- bool isIncomplete(Node q);
/** do instantiation round */
void doInstantiationRound(Theory::Effort effort);
/** Return true if this module should process quantified formula q */
}
+std::string ModelEngine::identify() const { return "ModelEngine"; }
+
bool ModelEngine::needsCheck( Theory::Effort e ) {
return e==Theory::EFFORT_LAST_CALL;
}
Node explain(TNode n) { return Node::null(); }
void debugPrint(const char* c);
/** Identify this module */
- std::string identify() const override { return "ModelEngine"; }
+ std::string identify() const override;
private:
/** Should we process quantified formula q? */
return true;
}
-bool InstMatchTrie::removeInstMatch(Node q,
- const std::vector<Node>& m,
- ImtIndexOrder* imtio,
- unsigned index)
-{
- Assert(index < q[0].getNumChildren());
- Assert(!imtio || index < imtio->d_order.size());
- unsigned i_index = imtio ? imtio->d_order[index] : index;
- Node n = m[i_index];
- std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
- if (it != d_data.end())
- {
- if ((index + 1) == q[0].getNumChildren()
- || (imtio && (index + 1) == imtio->d_order.size()))
- {
- d_data.erase(n);
- return true;
- }
- return it->second.removeInstMatch(q, m, imtio, index + 1);
- }
- return false;
-}
-
void InstMatchTrie::print(std::ostream& out,
Node q,
std::vector<TNode>& terms) const
return true;
}
-bool CDInstMatchTrie::removeInstMatch(Node q,
- const std::vector<Node>& m,
- unsigned index)
-{
- if (index == q[0].getNumChildren())
- {
- if (d_valid.get())
- {
- d_valid.set(false);
- return true;
- }
- return false;
- }
- std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
- if (it != d_data.end())
- {
- return it->second->removeInstMatch(q, m, index + 1);
- }
- return false;
-}
-
void CDInstMatchTrie::print(std::ostream& out,
Node q,
std::vector<TNode>& terms) const
ImtIndexOrder* imtio = nullptr,
bool onlyExist = false,
unsigned index = 0);
- /** remove inst match
- *
- * This removes (the suffix of) m starting at the given index from this trie.
- * It returns true if and only if this entry existed in this trie.
- * The domain of m is the bound variables of quantified formula q.
- */
- bool removeInstMatch(Node f,
- const std::vector<Node>& m,
- ImtIndexOrder* imtio = nullptr,
- unsigned index = 0);
/**
* Adds the instantiations for q into insts.
*/
const std::vector<Node>& m,
unsigned index = 0,
bool onlyExist = false);
- /** remove inst match
- *
- * This removes (the suffix of) m starting at the given index from this trie.
- * It returns true if and only if this entry existed in this trie.
- * The domain of m is the bound variables of quantified formula q.
- */
- bool removeInstMatch(Node q, const std::vector<Node>& m, unsigned index = 0);
/**
* Adds the instantiations for q into insts.
*/
return d_inst_match_trie[q].addInstMatch(q, terms);
}
-bool Instantiate::removeInstantiationInternal(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->removeInstMatch(q, terms);
- }
- return false;
- }
- return d_inst_match_trie[q].removeInstMatch(q, terms);
-}
-
void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const
{
for (NodeInstListMap::const_iterator it = d_insts.begin();
private:
/** record instantiation, return true if it was not a duplicate */
bool recordInstantiationInternal(Node q, const std::vector<Node>& terms);
- /** remove instantiation from the cache */
- bool removeInstantiationInternal(Node q, const std::vector<Node>& terms);
/**
* Ensure that n has type tn, return a term equivalent to it for that type
* if possible.
SynthEngine::~SynthEngine() {}
+std::string SynthEngine::identify() const { return "SynthEngine"; }
+
void SynthEngine::presolve()
{
Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
/* Called for new quantifiers */
void registerQuantifier(Node q) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const override { return "SynthEngine"; }
+ std::string identify() const override;
/** get synth solutions
*
* This function adds entries to sol_map that map functions-to-synthesize
projects / cvc5.git / commitdiff