summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp80
-rw-r--r--src/theory/quantifiers/fun_def_process.cpp11
-rw-r--r--src/theory/quantifiers/trigger.cpp29
-rw-r--r--src/theory/quantifiers/trigger.h3
-rw-r--r--src/theory/uf/theory_uf_type_rules.h4
5 files changed, 108 insertions, 19 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c03040868..83d14149b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -60,7 +60,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
d_equalityEngine.addFunctionKind(kind::DT_SIZE);
d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
- d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+ //d_equalityEngine.addFunctionKind(kind::APPLY_UF);
d_true = NodeManager::currentNM()->mkConst( true );
d_dtfCounter = 0;
@@ -1073,6 +1073,36 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
void TheoryDatatypes::computeCareGraph(){
Trace("dt-cg") << "Compute graph for dt..." << std::endl;
+ /*
+ Trace("dt-cg") << "Look at shared terms..." << std::endl;
+ for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
+ TNode a = d_sharedTerms[i];
+ if( a.getKind()!=APPLY_CONSTRUCTOR && a.getKind()!=APPLY_SELECTOR_TOTAL ){
+ TypeNode aType = a.getType();
+ for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
+ TNode b = d_sharedTerms[j];
+ if( b.getKind()!=APPLY_CONSTRUCTOR && b.getKind()!=APPLY_SELECTOR_TOTAL ){
+ if (b.getType() != aType) {
+ // We don't care about the terms of different types
+ continue;
+ }
+ switch (d_valuation.getEqualityStatus(a, b)) {
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ case EQUALITY_FALSE_AND_PROPAGATED:
+ // If we know about it, we should have propagated it, so we can skip
+ break;
+ default:
+ // Let's split on it
+ addCarePair(a, b);
+ break;
+ }
+ }
+ }
+ }
+ }
+ */
+
+ Trace("dt-cg") << "Look at theory terms..." << std::endl;
vector< pair<TNode, TNode> > currentPairs;
for( unsigned r=0; r<2; r++ ){
unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size();
@@ -1096,7 +1126,7 @@ void TheoryDatatypes::computeCareGraph(){
Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y);
- if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_UNKNOWN ){
+ if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
somePairIsDisequal = true;
break;
}else{
@@ -1174,11 +1204,26 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
//for all equivalence classes that are datatypes
if( DatatypesRewriter::isTermDatatype( eqc ) ){
EqcInfo* ei = getOrMakeEqcInfo( eqc );
- if( !ei->d_constructor.get().isNull() ){
- cons.push_back( ei->d_constructor.get() );
- eqc_cons[ eqc ] = ei->d_constructor.get();
+ if( ei && !ei->d_constructor.get().isNull() ){
+ Node c = ei->d_constructor.get();
+ cons.push_back( c );
+ eqc_cons[ eqc ] = c;
}else{
- nodes.push_back( eqc );
+ //if eqc contains a symbol known to datatypes (a selector), then we must assign
+ bool containsTSym = false;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+ while( !eqc_i.isFinished() ){
+ Node n = *eqc_i;
+ Trace("dt-cmi-debug") << n << " has kind " << n.getKind() << ", isVar = " << n.isVar() << std::endl;
+ if( n.isVar() || n.getKind()==APPLY_SELECTOR_TOTAL ){
+ containsTSym = true;
+ break;
+ }
+ ++eqc_i;
+ }
+ if( containsTSym ){
+ nodes.push_back( eqc );
+ }
}
}
++eqccs_i;
@@ -1199,6 +1244,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl;
TypeNode tn = eqc.getType();
//if it is infinite, make sure it is fresh
+ // this ensures that the term that this is an argument of is distinct.
if( eqc.getType().getCardinality().isInfinite() ){
std::map< TypeNode, int >::iterator it = typ_enum_map.find( tn );
int teIndex;
@@ -1753,7 +1799,7 @@ bool TheoryDatatypes::mustSpecifyAssignment(){
}
bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
- //the datatypes decision procedure makes 5 "internal" inferences apart from the equality engine :
+ //the datatypes decision procedure makes "internal" inferences apart from the equality engine :
// (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
// (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
// (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
@@ -1764,12 +1810,20 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
bool addLemma = false;
if( n.getKind()==EQUAL || n.getKind()==IFF ){
- TypeNode tn = n[0].getType();
- if( !tn.isDatatype() ){
- addLemma = true;
- }else{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- addLemma = dt.involvesExternalType();
+ for( unsigned i=0; i<2; i++ ){
+ if( n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){
+ addLemma = true;
+ }
+ }
+
+ if( !addLemma ){
+ TypeNode tn = n[0].getType();
+ if( !DatatypesRewriter::isTypeDatatype( tn ) ){
+ addLemma = true;
+ }else{
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ addLemma = dt.involvesExternalType();
+ }
}
//for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
// if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 0e365c875..cb772a31f 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -71,9 +71,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
}
Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << " to ";
+ Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
+ Trace("fmf-fun-def") << " to " << std::endl;
assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
- Trace("fmf-fun-def") << assertions[i] << std::endl;
+ Trace("fmf-fun-def") << " " << assertions[i] << std::endl;
fd_assertions.push_back( i );
}
}
@@ -86,7 +87,9 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
Assert( constraints.empty() );
if( n!=assertions[i] ){
n = Rewriter::rewrite( n );
- Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << " to " << n << std::endl;
+ Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl;
+ Trace("fmf-fun-def-rewrite") << " to " << std::endl;
+ Trace("fmf-fun-def-rewrite") << " " << n << std::endl;
assertions[i] = n;
}
}
@@ -139,7 +142,7 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co
}else{
//must add at higher level
}
- return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( AND, c );
+ return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( pol ? AND : OR, c );
}
}else{
//simplify term
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index b2b8e7197..511103019 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -385,6 +385,30 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
}
}
+bool Trigger::isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ) {
+ if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
+ bool hasVar = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==APPLY_UF ){
+ return false;
+ }else if( n[i].getKind()==INST_CONSTANT ){
+ hasVar = true;
+ //if( std::find( var_found.begin(), var_found.end(), n[i]
+ }
+ }
+ if( hasVar ){
+ patTerms.push_back( n );
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isLocalTheoryExt2( n, var_found, patTerms ) ){
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
bool Trigger::isBooleanTermTrigger( Node n ) {
if( n.getKind()==ITE ){
//check for boolean term converted to ITE
@@ -414,6 +438,11 @@ bool Trigger::isPureTheoryTrigger( Node n ) {
}
}
+bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& patTerms ) {
+ std::vector< Node > var_found;
+ return isLocalTheoryExt2( n, var_found, patTerms );
+}
+
void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){
std::map< Node, bool > patMap;
if( filterInst ){
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 75ada4f83..482701a82 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -95,6 +95,8 @@ private:
static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
/** collect all APPLY_UF pattern terms for f in n */
static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
+ /** is local theory extensions term */
+ static bool isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms );
public:
//different strategies for choosing trigger terms
enum {
@@ -111,6 +113,7 @@ public:
static bool isSimpleTrigger( Node n );
static bool isBooleanTermTrigger( Node n );
static bool isPureTheoryTrigger( Node n );
+ static bool isLocalTheoryExt( Node n, std::vector< Node >& patTerms );
/** return data structure for producing matches for this trigger. */
static InstMatchGenerator* getInstMatchGenerator( Node n );
static Node getInversionVariable( Node n );
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index c30742ac5..93fd1dc6f 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -91,8 +91,8 @@ public:
if( n[0].getKind()!=kind::CONST_RATIONAL ){
throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be a constant");
}
- if( n[0].getConst<Rational>().getNumerator().sgn()!=1 ){
- throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be positive");
+ if( n[0].getConst<Rational>().getNumerator().sgn()==-1 ){
+ throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be non-negative");
}
}
return nodeManager->booleanType();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback