summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/theory_model.cpp68
-rw-r--r--src/theory/theory_model.h3
-rw-r--r--test/regress/regress0/fmf/Makefile.am8
-rwxr-xr-xtest/regress/regress0/fmf/dt-proper-model.smt216
4 files changed, 91 insertions, 4 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index fb5fb0f0c..c6837ddf4 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -15,6 +15,7 @@
#include "options/smt_options.h"
#include "options/uf_options.h"
+#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
@@ -506,6 +507,43 @@ bool TheoryEngineModelBuilder::isCdtValueMatch( Node v, Node r, Node eqc, Node&
return false;
}
+bool TheoryEngineModelBuilder::involvesUSort( TypeNode tn ) {
+ if( tn.isSort() ){
+ return true;
+ }else if( tn.isArray() ){
+ return involvesUSort( tn.getArrayIndexType() ) || involvesUSort( tn.getArrayConstituentType() );
+ }else if( tn.isSet() ){
+ return involvesUSort( tn.getSetElementType() );
+ }else if( tn.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ return dt.involvesUninterpretedType();
+ }else{
+ return false;
+ }
+}
+
+bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ) {
+ Assert( v.isConst() );
+ if( visited.find( v )==visited.end() ){
+ visited[v] = true;
+ TypeNode tn = v.getType();
+ if( tn.isSort() ){
+ Trace("exc-value-debug") << "Is excluded usort value : " << v << " " << tn << std::endl;
+ unsigned card = eqc_usort_count[tn];
+ Trace("exc-value-debug") << " Cardinality is " << card << std::endl;
+ unsigned index = v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+ Trace("exc-value-debug") << " Index is " << index << std::endl;
+ return index>0 && index>=card;
+ }
+ for( unsigned i=0; i<v.getNumChildren(); i++ ){
+ if( isExcludedUSortValue( eqc_usort_count, v[i], visited ) ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
{
Trace("model-builder") << "TheoryEngineModelBuilder: buildModel, fullModel = " << fullModel << std::endl;
@@ -523,6 +561,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
d_te->collectModelInfo(tm, fullModel);
// Loop through all terms and make sure that assignable sub-terms are in the equality engine
+ // Also, record #eqc per type (for finite model finding)
+ std::map< TypeNode, unsigned > eqc_usort_count;
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
{
NodeSet cache;
@@ -531,6 +571,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
for ( ; !eqc_i.isFinished(); ++eqc_i) {
checkTerms(*eqc_i, tm, cache);
}
+ TypeNode tn = (*eqcs_i).getType();
+ if( tn.isSort() ){
+ if( eqc_usort_count.find( tn )==eqc_usort_count.end() ){
+ eqc_usort_count[tn] = 1;
+ }else{
+ eqc_usort_count[tn]++;
+ }
+ }
}
}
@@ -715,11 +763,16 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
if(t.isTuple() || t.isRecord()) {
t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
}
+ //get properties of this type
bool isCorecursive = false;
+ bool isUSortFiniteRestricted = false;
if( t.isDatatype() ){
const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() );
}
+ if( options::finiteModelFind() ){
+ isUSortFiniteRestricted = !t.isSort() && involvesUSort( t );
+ }
set<Node>* repSet = typeRepSet.getSet(t);
TypeNode tb = t.getBaseType();
if (!assignOne) {
@@ -756,14 +809,27 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
bool success;
do{
n = typeConstSet.nextTypeEnum(t, true);
+ //--- AJR: this code checks whether n is a legal value
success = true;
- if( isCorecursive ){
+ if( isUSortFiniteRestricted ){
+ //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc)
+ std::map< Node, bool > visited;
+ success = !isExcludedUSortValue( eqc_usort_count, n, visited );
+ if( !success ){
+ Trace("exc-value") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl;
+ }
+ }
+ if( success && isCorecursive ){
if (repSet != NULL && !repSet->empty()) {
// in the case of codatatypes, check if it is in the set of values that we cannot assign
// this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015
success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 );
+ if( !success ){
+ Trace("exc-value") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl;
+ }
}
}
+ //---
}while( !success );
}
else {
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index fb2c3cd01..8ee4e843d 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -260,6 +260,9 @@ protected:
/** is v an excluded codatatype value */
bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
+ /** involves usort */
+ bool involvesUSort( TypeNode tn );
+ bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited );
public:
TheoryEngineModelBuilder(TheoryEngine* te);
virtual ~TheoryEngineModelBuilder(){}
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index bca9f2e4f..5abadbcb8 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -20,7 +20,6 @@ MAKEFLAGS = -k
# put it below in "TESTS +="
TESTS = \
array_card.smt2 \
- agree466.smt2 \
ALG008-1.smt2 \
german169.smt2 \
QEpres-uf.855035.smt \
@@ -43,7 +42,8 @@ TESTS = \
syn002-si-real-int.smt2 \
krs-sat.smt2 \
forall_unit_data2.smt2 \
- sc_bad_model_1221.smt2
+ sc_bad_model_1221.smt2 \
+ dt-proper-model.smt2
EXTRA_DIST = $(TESTS)
@@ -54,11 +54,13 @@ EXTRA_DIST = $(TESTS)
#TESTS += \
# error.cvc
#endif
-#
+#
# and make sure to distribute it
#EXTRA_DIST += \
# error.cvc
+# agree466.smt2 timeout after commit on 1/14 due to Array+FMF model construction
+
# synonyms for "check" in this directory
.PHONY: regress regress0 test
regress regress0 test: check
diff --git a/test/regress/regress0/fmf/dt-proper-model.smt2 b/test/regress/regress0/fmf/dt-proper-model.smt2
new file mode 100755
index 000000000..60a0b6377
--- /dev/null
+++ b/test/regress/regress0/fmf/dt-proper-model.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-datatypes () ((D (cons (x Int) (y U)))))
+(declare-fun d1 () D)
+(declare-fun d2 () D)
+(declare-fun d3 () D)
+(declare-fun d4 () D)
+(assert (distinct d1 d2 d3 d4))
+(assert (forall ((x U) (y U)) (= x y)))
+(declare-fun a () U)
+(declare-fun P (U) Bool)
+(assert (P a))
+(check-sat) \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback