diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/arrays | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 1 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 9 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 42 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_instantiator.cpp | 56 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_instantiator.h | 51 |
6 files changed, 149 insertions, 14 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 3dde70145..57c55d765 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -15,6 +15,8 @@ libarrays_la_SOURCES = \ array_info.h \ array_info.cpp \ static_fact_manager.h \ - static_fact_manager.cpp + static_fact_manager.cpp \ + theory_arrays_instantiator.h \ + theory_arrays_instantiator.cpp EXTRA_DIST = kinds diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 06240a315..195a60035 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -6,6 +6,7 @@ theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" typechecker "theory/arrays/theory_arrays_type_rules.h" +instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h" properties polite stable-infinite parametric properties check propagate presolve diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 81661acd1..376a7e90f 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -23,6 +23,7 @@ #include <map> #include "theory/rewriter.h" #include "expr/command.h" +#include "theory/arrays/theory_arrays_instantiator.h" using namespace std; @@ -45,8 +46,8 @@ const bool d_solveWrite2 = false; const bool d_useNonLinearOpt = true; const bool d_eagerIndexSplitting = true; -TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo), +TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : + Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe), d_numRow("theory::arrays::number of Row lemmas", 0), d_numExt("theory::arrays::number of Ext lemmas", 0), d_numProp("theory::arrays::number of propagations", 0), @@ -218,7 +219,7 @@ Node TheoryArrays::ppRewrite(TNode term) { } Node r1 = nm->mkNode(kind::SELECT, e1, index_i); - conc = (r1.getType() == nm->booleanType())? + conc = (r1.getType() == nm->booleanType())? r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]); if (hyp.getNumChildren() != 0) { if (hyp.getNumChildren() == 1) { @@ -582,7 +583,6 @@ void TheoryArrays::computeCareGraph() // Get representative trigger terms TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY); TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAY); - EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared); switch (eqStatusDomain) { case EQUALITY_TRUE_AND_PROPAGATED: @@ -605,6 +605,7 @@ void TheoryArrays::computeCareGraph() break; } + // Otherwise, add this pair Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl; addCarePair(x_shared, y_shared); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 80fe692c0..1bf42a105 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -39,32 +39,32 @@ namespace arrays { * Overview of decision procedure: * * Preliminary notation: - * Stores(a) = {t | a ~ t and t = store( _ _ _ )} + * Stores(a) = {t | a ~ t and t = store( _ _ _ )} * InStores(a) = {t | t = store (b _ _) and a ~ b } * Indices(a) = {i | there exists a term b[i] such that a ~ b or store(b i v)} * ~ represents the equivalence relation based on the asserted equalities in the * current context. - * + * * The rules implemented are the following: * store(b i v) * Row1 ------------------- * store(b i v)[i] = v - * + * * store(b i v) a'[j] * Row ---------------------- [ a' ~ store(b i v) or a' ~ b ] * i = j OR a[j] = b[j] - * + * * a b same kind arrays * Ext ------------------------ [ a!= b in current context, k new var] * a = b OR a[k] != b[k]p - * - * + * + * * The Row1 one rule is implemented implicitly as follows: * - for each store(b i v) term add the following equality to the congruence * closure store(b i v)[i] = v * - if one of the literals in a conflict is of the form store(b i v)[i] = v * remove it from the conflict - * + * * Because new store terms are not created, we need to check if we need to * instantiate a new Row axiom in the following cases: * 1. the congruence relation changes (i.e. two terms get merged) @@ -77,7 +77,7 @@ namespace arrays { * - this is implemented in the checkRowForIndex method which is called * when preregistering a term of the form a[i]. * - as a consequence lemmas are instantiated even before full effort check - * + * * The Ext axiom is instantiated when a disequality is asserted during full effort * check. Ext lemmas are stored in a cache to prevent instantiating essentially * the same lemma multiple times. @@ -122,7 +122,7 @@ class TheoryArrays : public Theory { public: - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); ~TheoryArrays(); std::string identify() const { return std::string("TheoryArrays"); } @@ -133,6 +133,16 @@ class TheoryArrays : public Theory { private: + // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used + class PPNotifyClass { + public: + bool notify(TNode propagation) { return true; } + void notify(TNode t1, TNode t2) { } + }; + + /** The notify class for d_ppEqualityEngine */ + PPNotifyClass d_ppNotify; + /** Equaltity engine */ eq::EqualityEngine d_ppEqualityEngine; @@ -181,6 +191,15 @@ class TheoryArrays : public Theory { private: + class MayEqualNotifyClass { + public: + bool notify(TNode propagation) { return true; } + void notify(TNode t1, TNode t2) { } + }; + + /** The notify class for d_mayEqualEqualityEngine */ + MayEqualNotifyClass d_mayEqualNotify; + /** Equaltity engine for determining if two arrays might be equal */ eq::EqualityEngine d_mayEqualEqualityEngine; @@ -270,6 +289,11 @@ class TheoryArrays : public Theory { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_arrays.conflict(t1, t2); } + + void eqNotifyNewClass(TNode t) { } + void eqNotifyPreMerge(TNode t1, TNode t2) { } + void eqNotifyPostMerge(TNode t1, TNode t2) { } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } }; /** The notify class for d_equalityEngine */ diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp new file mode 100644 index 000000000..334d70eea --- /dev/null +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -0,0 +1,56 @@ +/********************* */ +/*! \file theory_arrays_instantiator.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory_arrays_instantiator class + **/ + +#include "theory/theory_engine.h" +#include "theory/arrays/theory_arrays_instantiator.h" +#include "theory/arrays/theory_arrays.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::arrays; + +InstantiatorTheoryArrays::InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th) : +Instantiator( c, ie, th ){ + +} + +void InstantiatorTheoryArrays::preRegisterTerm( Node t ){ + +} + +void InstantiatorTheoryArrays::assertNode( Node assertion ){ + Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl; + d_quantEngine->addTermToDatabase( assertion ); + if( Options::current()->cbqi ){ + if( assertion.hasAttribute(InstConstantAttribute()) ){ + setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); + }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ + setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) ); + } + } +} + + +void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort effort ){ + +} + +int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e, int limitInst ){ + return InstStrategy::STATUS_SAT; +} diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h new file mode 100644 index 000000000..6a7c9c3ed --- /dev/null +++ b/src/theory/arrays/theory_arrays_instantiator.h @@ -0,0 +1,51 @@ +/********************* */ +/*! \file theory_arrays_instantiator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Instantiator for theory of arrays + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__INSTANTIATOR_THEORY_ARRAYS_H +#define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +class InstantiatorTheoryArrays : public Instantiator{ + friend class QuantifiersEngine; +protected: + /** reset instantiation round */ + void processResetInstantiationRound( Theory::Effort effort ); + /** process quantifier */ + int process( Node f, Theory::Effort effort, int e, int limitInst = 0 ); +public: + InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th); + ~InstantiatorTheoryArrays() {} + /** Pre-register a term. */ + void preRegisterTerm( Node t ); + /** assertNode function, assertion is asserted to theory */ + void assertNode( Node assertion ); + /** identify */ + std::string identify() const { return std::string("InstantiatorTheoryArrays"); } +};/* class Instantiatior */ + +} +} +} + +#endif
\ No newline at end of file |