summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/arith_rewriter.cpp19
-rw-r--r--src/theory/arith/kinds20
-rw-r--r--src/theory/arith/theory_arith_type_rules.h34
-rw-r--r--src/theory/builtin/kinds13
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h20
-rw-r--r--src/theory/substitutions.cpp5
-rw-r--r--src/theory/substitutions.h22
-rw-r--r--src/theory/theory.cpp9
-rw-r--r--src/theory/theory.h8
-rw-r--r--src/theory/theory_engine.cpp6
-rw-r--r--src/theory/theory_engine.h2
11 files changed, 150 insertions, 8 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a309b9403..c0ef02ec4 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -93,6 +93,21 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
return preRewritePlus(t);
}else if(t.getKind() == kind::MULT){
return preRewriteMult(t);
+ }else if(t.getKind() == kind::INTS_DIVISION){
+ Integer intOne(1);
+ if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
+ return RewriteResponse(REWRITE_AGAIN, t[0]);
+ }else{
+ return RewriteResponse(REWRITE_DONE, t);
+ }
+ }else if(t.getKind() == kind::INTS_MODULUS){
+ Integer intOne(1);
+ if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
+ Integer intZero(0);
+ return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero));
+ }else{
+ return RewriteResponse(REWRITE_DONE, t);
+ }
}else{
Unreachable();
}
@@ -112,6 +127,10 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
return postRewritePlus(t);
}else if(t.getKind() == kind::MULT){
return postRewriteMult(t);
+ }else if(t.getKind() == kind::INTS_DIVISION){
+ return RewriteResponse(REWRITE_DONE, t);
+ }else if(t.getKind() == kind::INTS_MODULUS){
+ return RewriteResponse(REWRITE_DONE, t);
}else{
Unreachable();
}
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index bf5ea24c1..95d7d6ed1 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -17,7 +17,9 @@ operator PLUS 2: "arithmetic addition"
operator MULT 2: "arithmetic multiplication"
operator MINUS 2 "arithmetic binary subtraction operator"
operator UMINUS 1 "arithmetic unary negation"
-operator DIVISION 2 "arithmetic division"
+operator DIVISION 2 "real division"
+operator INTS_DIVISION 2 "ints division"
+operator INTS_MODULUS 2 "ints modulus"
operator POW 2 "arithmetic power"
sort REAL_TYPE \
@@ -39,6 +41,19 @@ sort PSEUDOBOOLEAN_TYPE \
"expr/node_manager.h" \
"Pseudoboolean type"
+constant SUBRANGE_TYPE \
+ ::CVC4::SubrangeBounds \
+ ::CVC4::SubrangeBoundsHashStrategy \
+ "util/subrange_bound.h" \
+ "the type of an integer subrange"
+cardinality SUBRANGE_TYPE \
+ "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \
+ "theory/arith/theory_arith_type_rules.h"
+well-founded SUBRANGE_TYPE \
+ true \
+ "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
+ "theory/arith/theory_arith_type_rules.h"
+
constant CONST_RATIONAL \
::CVC4::Rational \
::CVC4::RationalHashStrategy \
@@ -75,4 +90,7 @@ typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
+typerule INTS_DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule INTS_MODULUS ::CVC4::theory::arith::ArithOperatorTypeRule
+
endtheory
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 511982d48..8d0d79f0a 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -21,6 +21,8 @@
#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
#define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#include "util/subrange_bound.h"
+
namespace CVC4 {
namespace theory {
namespace arith {
@@ -33,7 +35,7 @@ public:
if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
return nodeManager->integerType();
}
-};
+};/* class ArithConstantTypeRule */
class ArithOperatorTypeRule {
public:
@@ -60,7 +62,7 @@ public:
}
return (isInteger ? integerType : realType);
}
-};
+};/* class ArithOperatorTypeRule */
class ArithPredicateTypeRule {
public:
@@ -80,7 +82,33 @@ public:
}
return nodeManager->booleanType();
}
-};
+};/* class ArithPredicateTypeRule */
+
+class SubrangeProperties {
+public:
+ inline static Cardinality computeCardinality(TypeNode type) {
+ Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+ const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
+ if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) {
+ return Cardinality::INTEGERS;
+ }
+ return Cardinality(bounds.upper.getBound() - bounds.lower.getBound());
+ }
+
+ inline static Node mkGroundTerm(TypeNode type) {
+ Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+ const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
+ if(bounds.lower.hasBound()) {
+ return NodeManager::currentNM()->mkConst(bounds.lower.getBound());
+ }
+ if(bounds.upper.hasBound()) {
+ return NodeManager::currentNM()->mkConst(bounds.upper.getBound());
+ }
+ return NodeManager::currentNM()->mkConst(Integer(0));
+ }
+};/* class SubrangeProperties */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 61abfbfaf..519536c81 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -325,4 +325,17 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
+constant SUBTYPE_TYPE \
+ ::CVC4::Predicate \
+ ::CVC4::PredicateHashStrategy \
+ "util/predicate.h" \
+ "predicate subtype"
+cardinality SUBTYPE_TYPE \
+ "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \
+ "theory/builtin/theory_builtin_type_rules.h"
+well-founded SUBTYPE_TYPE \
+ "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \
+ "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \
+ "theory/builtin/theory_builtin_type_rules.h"
+
endtheory
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index cd3e1437f..706196f8b 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -227,6 +227,26 @@ public:
}
};/* class TupleProperties */
+class SubtypeProperties {
+public:
+
+ inline static Cardinality computeCardinality(TypeNode type) {
+ Assert(type.getKind() == kind::SUBTYPE_TYPE);
+ Unimplemented("Computing the cardinality for predicate subtype not yet supported.");
+ }
+
+ inline static bool isWellFounded(TypeNode type) {
+ Assert(type.getKind() == kind::SUBTYPE_TYPE);
+ Unimplemented("Computing the well-foundedness for predicate subtype not yet supported.");
+ }
+
+ inline static Node mkGroundTerm(TypeNode type) {
+ Assert(type.getKind() == kind::SUBTYPE_TYPE);
+ Unimplemented("Constructing a ground term for predicate subtype not yet supported.");
+ }
+
+};/* class SubtypeProperties */
+
}/* CVC4::theory::builtin namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 301cb8d60..caf7566b9 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -173,4 +173,9 @@ void SubstitutionMap::print(ostream& out) const {
}
}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
+ return out << "[CDMap-iterator]";
+}
+
}/* CVC4 namespace */
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index c03baa1ac..1ade4815d 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -48,6 +48,9 @@ public:
typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap;
+ typedef NodeMap::iterator iterator;
+ typedef NodeMap::const_iterator const_iterator;
+
private:
typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
@@ -115,6 +118,22 @@ public:
return const_cast<SubstitutionMap*>(this)->apply(t);
}
+ iterator begin() {
+ return d_substitutions.begin();
+ }
+
+ iterator end() {
+ return d_substitutions.end();
+ }
+
+ const_iterator begin() const {
+ return d_substitutions.begin();
+ }
+
+ const_iterator end() const {
+ return d_substitutions.end();
+ }
+
// NOTE [MGD]: removed clear() and swap() from the interface
// when this data structure became context-dependent
// because they weren't used---and it's not clear how they
@@ -134,6 +153,9 @@ inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subs
}
}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i);
+
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__SUBSTITUTIONS_H */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 1998498f5..76aabeb1f 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -76,5 +76,14 @@ void Theory::computeCareGraph(CareGraph& careGraph) {
}
}
+void Theory::printFacts(std::ostream& os) const {
+ unsigned i, n = d_facts.size();
+ for(i = 0; i < n; i++){
+ const Assertion& a_i = d_facts[i];
+ Node assertion = a_i;
+ os << d_id << '[' << i << ']' << " " << assertion << endl;
+ }
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b0f5e4e53..35c81239f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -142,7 +142,7 @@ private:
protected:
- /**
+ /**
* A list of shared terms that the theory has.
*/
context::CDList<TNode> d_sharedTerms;
@@ -210,6 +210,9 @@ protected:
*/
static TheoryId s_uninterpretedSortOwner;
+ void printFacts(std::ostream& os) const;
+
+
public:
/**
@@ -218,6 +221,9 @@ public:
static inline TheoryId theoryOf(TypeNode typeNode) {
Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl;
TheoryId id;
+ while (typeNode.isPredicateSubtype()) {
+ typeNode = typeNode.getSubtypeBaseType();
+ }
if (typeNode.getKind() == kind::TYPE_CONSTANT) {
id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
} else {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 91d6beead..2950ad413 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -575,8 +575,10 @@ void TheoryEngine::assertFact(TNode node)
// Get the atom
TNode atom = node.getKind() == kind::NOT ? node[0] : node;
- // Assert the fact to the apropriate theory
- theoryOf(atom)->assertFact(node, true);
+ // Assert the fact to the appropriate theory and mark it active
+ Theory* theory = theoryOf(atom);
+ theory->assertFact(node, true);
+ markActive(Theory::setInsert(theory->getId()));
// If any shared terms, notify the theories
if (d_sharedTerms.hasSharedTerms(atom)) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ceefa88e8..72244a573 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -91,7 +91,7 @@ class TheoryEngine {
/**
* A bitmap of theories that are "active" for the current run. We
- * mark a theory active when we firt see a term or type belonging to
+ * mark a theory active when we first see a term or type belonging to
* it. This is important because we can optimize for single-theory
* runs (no sharing), can reduce the cost of walking the DAG on
* registration, etc.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback