summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/datatypes/datatypes_rewriter.h64
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp114
-rw-r--r--src/theory/datatypes/theory_datatypes.h2
-rw-r--r--src/theory/datatypes/type_enumerator.cpp6
-rw-r--r--src/theory/datatypes/type_enumerator.h3
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp10
-rw-r--r--src/theory/quantifiers/first_order_model.cpp24
-rw-r--r--src/theory/quantifiers/first_order_model.h3
-rw-r--r--src/theory/quantifiers/full_model_check.cpp125
-rw-r--r--src/theory/quantifiers/full_model_check.h8
-rw-r--r--src/theory/quantifiers/term_database.cpp10
-rw-r--r--src/theory/quantifiers_engine.cpp4
-rw-r--r--src/theory/theory_model.cpp11
-rw-r--r--src/theory/theory_model.h1
-rw-r--r--src/theory/uf/theory_uf.cpp2
15 files changed, 212 insertions, 175 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index da2282a2c..1e7e714cf 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -167,19 +167,19 @@ public:
//typically should not be called
TypeNode tn = in.getType();
Node gt;
- if( tn.isSort() ){
+ bool useTe = true;
+ //if( !tn.isSort() ){
+ // useTe = false;
+ //}
+ if( isTypeDatatype( tn ) ){
+ const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
+ useTe = !dta.isCodatatype();
+ }
+ if( useTe ){
TypeEnumerator te(tn);
gt = *te;
}else{
- //check whether well-founded
- //bool isWf = true;
- //if( isTypeDatatype( tn ) ){
- // const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
- // isWf = dta.isWellFounded();
- //}
- //if( isWf || in[0].isConst() ){
gt = tn.mkGroundTerm();
- //}
}
if( !gt.isNull() ){
//Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
@@ -531,28 +531,32 @@ private:
}
//eqc_stack stores depth
static Node normalizeCodatatypeConstantEqc( Node n, std::map< int, int >& eqc_stack, std::map< Node, int >& eqc, int depth ){
- Assert( eqc.find( n )!=eqc.end() );
- int e = eqc[n];
- std::map< int, int >::iterator it = eqc_stack.find( e );
- if( it!=eqc_stack.end() ){
- int debruijn = depth - it->second - 1;
- return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn));
+ Trace("dt-nconst-debug") << "normalizeCodatatypeConstantEqc: " << n << " depth=" << depth << std::endl;
+ if( eqc.find( n )==eqc.end() ){
+ return n;
}else{
- std::vector< Node > children;
- bool childChanged = false;
- eqc_stack[e] = depth;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nc = normalizeCodatatypeConstantEqc( n[i], eqc_stack, eqc, depth+1 );
- children.push_back( nc );
- childChanged = childChanged || nc!=n[i];
- }
- eqc_stack.erase(e);
- if( childChanged ){
- Assert( n.getKind()==kind::APPLY_CONSTRUCTOR );
- children.insert( children.begin(), n.getOperator() );
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ int e = eqc[n];
+ std::map< int, int >::iterator it = eqc_stack.find( e );
+ if( it!=eqc_stack.end() ){
+ int debruijn = depth - it->second - 1;
+ return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn));
}else{
- return n;
+ std::vector< Node > children;
+ bool childChanged = false;
+ eqc_stack[e] = depth;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = normalizeCodatatypeConstantEqc( n[i], eqc_stack, eqc, depth+1 );
+ children.push_back( nc );
+ childChanged = childChanged || nc!=n[i];
+ }
+ eqc_stack.erase(e);
+ if( childChanged ){
+ Assert( n.getKind()==kind::APPLY_CONSTRUCTOR );
+ children.insert( children.begin(), n.getOperator() );
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }else{
+ return n;
+ }
}
}
}
@@ -675,7 +679,7 @@ public:
eqc[it->first] = eqc[it->second];
}
//we now have a partition of equivalent terms
- Trace("dt-nconst") << "Equivalence classes ids : " << std::endl;
+ Trace("dt-nconst") << "Computed equivalence classes ids : " << std::endl;
for( std::map< Node, int >::iterator it = eqc.begin(); it != eqc.end(); ++it ){
Trace("dt-nconst") << " " << it->first << " -> " << it->second << std::endl;
}
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 439fd0cfb..c8d7338a7 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -268,12 +268,13 @@ void TheoryDatatypes::check(Effort e) {
}
if( needSplit && consIndex!=-1 ) {
- //if only one constructor, then this term must be this constructor
if( dt.getNumConstructors()==1 ){
+ //this may not be necessary?
+ //if only one constructor, then this term must be this constructor
Node t = DatatypesRewriter::mkTester( n, 0, dt );
d_pending.push_back( t );
d_pending_exp[ t ] = d_true;
- Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
+ Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl;
d_infer.push_back( t );
}else{
if( options::dtBinarySplit() ){
@@ -402,11 +403,14 @@ void TheoryDatatypes::doPendingMerges(){
d_pending_merge.clear();
}
-void TheoryDatatypes::doSendLemma( Node lem ) {
+bool TheoryDatatypes::doSendLemma( Node lem ) {
if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : " << lem << std::endl;
d_lemmas_produced_c[lem] = true;
d_out->lemma( lem );
+ return true;
+ }else{
+ return false;
}
}
@@ -440,7 +444,6 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_sym_break->d_lemmas[i] << std::endl;
doSendLemma( d_sygus_sym_break->d_lemmas[i] );
}
- Trace("dt-lemma-sygus") << "No lemmas" << std::endl;
d_sygus_sym_break->d_lemmas.clear();
/*
if( d_sygus_util->d_conflict ){
@@ -1124,8 +1127,8 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
nb << (*i);
Assert( (*i).getKind()==NOT );
Node t_arg2;
- int tindex = DatatypesRewriter::isTester( (*i)[0], t_arg2 );
- Assert( tindex!=-1 );
+ DatatypesRewriter::isTester( (*i)[0], t_arg2 );
+ //Assert( tindex!=-1 );
if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){
eq_terms.push_back( t_arg2 );
if( t_arg2!=t_arg ){
@@ -1569,46 +1572,31 @@ void TheoryDatatypes::collectTerms( Node n ) {
if( n.getKind() == APPLY_CONSTRUCTOR ){
Debug("datatypes") << " Found constructor " << n << endl;
d_consTerms.push_back( n );
- }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){
- d_selTerms.push_back( n );
- //we must also record which selectors exist
- Trace("dt-collapse-sel") << " Found selector " << n << endl;
- Node rep = getRepresentative( n[0] );
- //record it in the selectors
- EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
- //add it to the eqc info
- addSelector( n, eqc, rep );
-
- if( n.getKind() == DT_SIZE ){
- Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n );
- //must be non-negative
- Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl;
- d_pending.push_back( conc );
- d_pending_exp[ conc ] = d_true;
- d_infer.push_back( conc );
-/*
- //add size = 0 lemma
- Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) );
- std::vector< Node > children;
- children.push_back( nn.negate() );
- const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
- Node test = DatatypesRewriter::mkTester( n[0], i, dt );
- children.push_back( test );
- }
- }
- conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
- Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl;
- d_pending.push_back( conc );
- d_pending_exp[ conc ] = d_true;
- d_infer.push_back( conc );
-*/
- }
+ }else{
- if( n.getKind() == DT_HEIGHT_BOUND ){
- if( n[1].getConst<Rational>().isZero() ){
+ if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){
+ d_selTerms.push_back( n );
+ //we must also record which selectors exist
+ Trace("dt-collapse-sel") << " Found selector " << n << endl;
+ Node rep = getRepresentative( n[0] );
+ //record it in the selectors
+ EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
+ //add it to the eqc info
+ addSelector( n, eqc, rep );
+
+ if( n.getKind() == DT_SIZE ){
+ Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n );
+ //must be non-negative
+ Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl;
+ //d_pending.push_back( conc );
+ //d_pending_exp[ conc ] = d_true;
+ //d_infer.push_back( conc );
+ d_pending_lem.push_back( conc );
+ /*
+ //add size = 0 lemma
+ Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) );
std::vector< Node > children;
+ children.push_back( nn.negate() );
const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
@@ -1616,16 +1604,36 @@ void TheoryDatatypes::collectTerms( Node n ) {
children.push_back( test );
}
}
- Node lem;
- if( children.empty() ){
- lem = n.negate();
- }else{
- lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
+ conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+ Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl;
+ d_pending.push_back( conc );
+ d_pending_exp[ conc ] = d_true;
+ d_infer.push_back( conc );
+ */
+ }
+
+ if( n.getKind() == DT_HEIGHT_BOUND ){
+ if( n[1].getConst<Rational>().isZero() ){
+ std::vector< Node > children;
+ const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
+ Node test = DatatypesRewriter::mkTester( n[0], i, dt );
+ children.push_back( test );
+ }
+ }
+ Node lem;
+ if( children.empty() ){
+ lem = n.negate();
+ }else{
+ lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
+ }
+ Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
+ //d_pending.push_back( lem );
+ //d_pending_exp[ lem ] = d_true;
+ //d_infer.push_back( lem );
+ d_pending_lem.push_back( lem );
}
- Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
- d_pending.push_back( lem );
- d_pending_exp[ lem ] = d_true;
- d_infer.push_back( lem );
}
}
}
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 4dd621c86..d56538b2a 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -203,7 +203,7 @@ private:
/** do pending merged */
void doPendingMerges();
/** do send lemma */
- void doSendLemma( Node lem );
+ bool doSendLemma( Node lem );
/** get or make eqc info */
EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 57d16d31c..62446a937 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -170,7 +170,9 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
Debug("dt-enum") << "datatype is " << d_type << std::endl;
- Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl;
+ Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton();
+ Debug("dt-enum") << " " << d_datatype.isFinite() << std::endl;
+ Debug("dt-enum") << " " << d_datatype.isUFinite() << std::endl;
if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
//start with uninterpreted constant
@@ -218,4 +220,4 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
//set up initial conditions (should always succeed)
++*this; //increment( d_ctor );
AlwaysAssert( !isFinished() );
-} \ No newline at end of file
+}
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 67dabafe4..921ba403c 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -23,6 +23,7 @@
#include "expr/type_node.h"
#include "expr/type.h"
#include "expr/kind.h"
+#include "options/quantifiers_options.h"
namespace CVC4 {
namespace theory {
@@ -158,7 +159,7 @@ public:
}
if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){
//try next size limit as long as new terms were generated at last size, or other cases
- if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isFinite() ){
+ if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || ( options::finiteModelFind() ? !d_datatype.isUFinite() : !d_datatype.isFinite() ) ){
d_size_limit++;
d_ctor = d_zeroCtor;
for( unsigned i=0; i<d_sel_sum.size(); i++ ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index cc0b18ffe..345a5eaef 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -463,9 +463,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
lem = Rewriter::rewrite( lem );
Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl;
Trace("cegqi-engine") << " ...refine candidate." << std::endl;
- d_quantEngine->addLemma( lem );
- ++(d_statistics.d_cegqi_lemmas_refine);
- conj->d_refine_count++;
+ bool res = d_quantEngine->addLemma( lem );
+ if( res ){
+ ++(d_statistics.d_cegqi_lemmas_refine);
+ conj->d_refine_count++;
+ }else{
+ Trace("cegqi-engine") << " ...FAILED to add refinement!" << std::endl;
+ }
}
}
conj->d_ce_sk.clear();
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index aa2a43fbf..272f16be8 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -90,15 +90,19 @@ void FirstOrderModel::initialize() {
}
processInitializeQuantifier( f );
//initialize relevant models within bodies of all quantifiers
- initializeModelForTerm( f[1] );
+ std::map< Node, bool > visited;
+ initializeModelForTerm( f[1], visited );
}
processInitialize( false );
}
-void FirstOrderModel::initializeModelForTerm( Node n ){
- processInitializeModelForTerm( n );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- initializeModelForTerm( n[i] );
+void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& visited ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ processInitializeModelForTerm( n );
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ initializeModelForTerm( n[i], visited );
+ }
}
}
@@ -574,15 +578,6 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl;
}
}
-/*
- Node r = getRepresentative(n);
- if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){
- if (r==d_model_basis_rep[tn]) {
- r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
- }
- }
- return r;
-*/
return getRepresentative(n);
}
}
@@ -609,7 +604,6 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) {
for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
it->second->reset();
}
- d_model_basis_rep.clear();
}
}
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index a31e85d7e..d42eb61e3 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -67,7 +67,7 @@ public: //for Theory Quantifiers:
/** get number to reduce quantifiers */
unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); }
/** initialize model for term */
- void initializeModelForTerm( Node n );
+ void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
virtual void processInitializeModelForTerm( Node n ) = 0;
virtual void processInitializeQuantifier( Node q ) {}
public:
@@ -169,7 +169,6 @@ class FirstOrderModelFmc : public FirstOrderModel
private:
/** models for UF */
std::map<Node, Def * > d_models;
- std::map<TypeNode, Node > d_model_basis_rep;
std::map<TypeNode, Node > d_type_star;
Node intervalOp;
Node getUsedRepresentative(Node n, bool strict = false);
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index f0858f4e9..00a5241f5 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -325,11 +325,46 @@ QModelBuilder( c, qe ){
d_false = NodeManager::currentNM()->mkConst(false);
}
+void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
+ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
+ if( !fullModel ){
+ Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
+ d_preinitialized_types.clear();
+ //traverse equality engine
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+ std::map< TypeNode, int > typ_num;
+ while( !eqcs_i.isFinished() ){
+ TypeNode tr = (*eqcs_i).getType();
+ d_preinitialized_types[tr] = true;
+ ++eqcs_i;
+ }
+
+ //must ensure model basis terms exists in model for each relevant type
+ fm->initialize();
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node op = it->first;
+ TypeNode tno = op.getType();
+ for( unsigned i=0; i<tno.getNumChildren(); i++) {
+ preInitializeType( fm, tno[i] );
+ }
+ }
+ //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
+ if( !options::fmfEmptySorts() ){
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node q = fm->getAssertedQuantifier( i );
+ //make sure all types are set
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ preInitializeType( fm, q[0][i].getType() );
+ }
+ }
+ }
+ }
+}
+
void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
if( !fullModel ){
Trace("fmc") << "---Full Model Check reset() " << std::endl;
- fm->initialize();
d_quant_models.clear();
d_rep_ids.clear();
d_star_insts.clear();
@@ -338,50 +373,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
it != fm->d_rep_set.d_type_reps.end(); ++it ){
if( it->first.isSort() ){
Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
- Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
- Node rmbt = fm->getUsedRepresentative( mbt);
- int mbt_index = -1;
- Trace("fmc") << " Model basis term : " << mbt << std::endl;
for( size_t a=0; a<it->second.size(); a++ ){
Node r = fm->getUsedRepresentative( it->second[a] );
- std::vector< Node > eqc;
- ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
- Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);
- Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
- //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
- Trace("fmc-model-debug") << " {";
- //find best selection for representative
- for( size_t i=0; i<eqc.size(); i++ ){
- Trace("fmc-model-debug") << eqc[i] << ", ";
- }
- Trace("fmc-model-debug") << "}" << std::endl;
-
- //if this is the model basis eqc, replace with actual model basis term
- if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {
- fm->d_model_basis_rep[it->first] = r;
- r = mbt;
- mbt_index = a;
+ if( Trace.isOn("fmc-model-debug") ){
+ std::vector< Node > eqc;
+ ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+ Trace("fmc-model-debug") << " " << (it->second[a]==r);
+ Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+ //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+ Trace("fmc-model-debug") << " {";
+ for( size_t i=0; i<eqc.size(); i++ ){
+ Trace("fmc-model-debug") << eqc[i] << ", ";
+ }
+ Trace("fmc-model-debug") << "}" << std::endl;
}
d_rep_ids[it->first][r] = (int)a;
}
Trace("fmc-model-debug") << std::endl;
-
- if (mbt_index==-1) {
- std::cout << " WARNING: model basis term is not a representative!" << std::endl;
- exit(0);
- }else{
- Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;
- }
- }
- }
- //also process non-rep set sorts
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- Node op = it->first;
- TypeNode tno = op.getType();
- for( unsigned i=0; i<tno.getNumChildren(); i++) {
- initializeType( fm, tno[i] );
}
}
+
//now, make models
for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
Node op = it->first;
@@ -433,24 +444,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
entry_children.push_back(op);
bool hasNonStar = false;
for( unsigned i=0; i<c.getNumChildren(); i++) {
- Node ri = fm->getUsedRepresentative( c[i]);
- if( !ri.getType().isSort() && !ri.isConst() ){
- Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;
- Assert( false );
- }
+ Node ri = fm->getUsedRepresentative( c[i] );
children.push_back(ri);
+ bool isStar = false;
if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
if (fm->isModelBasisTerm(ri) ) {
ri = fm->getStar( ri.getType() );
+ isStar = true;
}else{
hasNonStar = true;
}
}
+ if( !isStar && !ri.isConst() ){
+ Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
+ Assert( false );
+ }
entry_children.push_back(ri);
}
Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
Node nv = fm->getUsedRepresentative( v );
- if( !nv.getType().isSort() && !nv.isConst() ){
+ if( !nv.isConst() ){
Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;
Assert( false );
}
@@ -523,20 +536,15 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
}
}
-void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
- if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){
- Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl;
- Node mbn;
- if (!fm->d_rep_set.hasType(tn)) {
- mbn = fm->getSomeDomainElement(tn);
- }else{
- mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
+ if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
+ d_preinitialized_types[tn] = true;
+ Node mb = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+ if( !mb.isConst() ){
+ Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl;
+ fm->d_equalityEngine->addTerm( mb );
+ fm->addTerm( mb );
}
- Trace("fmc") << "Get used rep for " << mbn << std::endl;
- Node mbnr = fm->getUsedRepresentative( mbn );
- Trace("fmc") << "...got " << mbnr << std::endl;
- fm->d_model_basis_rep[tn] = mbnr;
- Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;
}
}
@@ -591,10 +599,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" );
d_quant_cond[f] = op;
}
- //make sure all types are set
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- initializeType( fmfmc, f[0][i].getType() );
- }
if( options::mbqiMode()==MBQI_NONE ){
//just exhaustive instantiate
@@ -643,6 +647,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
Node ev = d_quant_models[f].evaluate(fmfmc, inst);
if (ev==d_true) {
addInst = false;
+ Trace("fmc-debug") << "...do not instantiate, evaluation was " << ev << std::endl;
}
}else{
//for debugging
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 29913d98d..c7bfcd189 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -92,8 +92,9 @@ protected:
std::map<Node, Node > d_quant_cond;
std::map< TypeNode, Node > d_array_cond;
std::map< Node, Node > d_array_term_cond;
- std::map<Node, std::vector< int > > d_star_insts;
- void initializeType( FirstOrderModelFmc * fm, TypeNode tn );
+ std::map< Node, std::vector< int > > d_star_insts;
+ std::map< TypeNode, bool > d_preinitialized_types;
+ void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
protected:
@@ -142,7 +143,8 @@ public:
Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
- /** process build model */
+ /** process build model */
+ void preProcessBuildModel(TheoryModel* m, bool fullModel);
void processBuildModel(TheoryModel* m, bool fullModel);
/** get current model value */
Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6dfd4c737..8bc9689bd 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -971,7 +971,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
}
ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind );
}
- Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
+ Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
//if it has an instantiation level, set the skolemized body to that level
if( f.hasAttribute(InstLevelAttribute()) ){
theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) );
@@ -1002,6 +1002,14 @@ Node TermDb::getSkolemizedBody( Node f ){
d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
}
}
+ if( Trace.isOn("quantifiers-sk") ){
+ Trace("quantifiers-sk") << "Skolemize : ";
+ for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
+ Trace("quantifiers-sk") << d_skolem_constants[f][i] << " ";
+ }
+ Trace("quantifiers-sk") << "for " << std::endl;
+ Trace("quantifiers-sk") << " " << f << std::endl;
+ }
}
return d_skolem_body[ f ];
}
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index aee3ac4b8..19d66165a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -602,9 +602,9 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
NodeBuilder<> nb(kind::OR);
nb << f << body.notNode();
Node lem = nb;
- if( Trace.isOn("quantifiers-sk") ){
+ if( Trace.isOn("quantifiers-sk-debug") ){
Node slem = Rewriter::rewrite( lem );
- Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl;
+ Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
}
getOutputChannel().lemma( lem, false, true );
d_skolemized[f] = true;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index a61df11d8..d024e0270 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -114,7 +114,8 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c
return (*it).second;
}
Node ret = n;
- if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
+ if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ||
+ ( n.getKind() == kind::CARDINALITY_CONSTRAINT && options::ufssMode()!=theory::uf::UF_SS_FULL ) ) {
// We should have terms, thanks to TheoryQuantifiers::collectModelInfo().
// However, if the Decision Engine stops us early, there might be a
// quantifier that isn't assigned. In conjunction with miniscoping, this
@@ -570,6 +571,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
d_te->collectModelInfo(tm, fullModel);
+ // model-builder specific initialization
+ preProcessBuildModel(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;
@@ -830,6 +835,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
if (t.getCardinality().isInfinite()) {
bool success;
do{
+ Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl;
n = typeConstSet.nextTypeEnum(t, true);
//--- AJR: this code checks whether n is a legal value
Assert( !n.isNull() );
@@ -1016,6 +1022,9 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
return retNode;
}
+void TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) {
+
+}
void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
{
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 4b27aeacb..b0952538a 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -255,6 +255,7 @@ protected:
typedef std::hash_set<Node, NodeHashFunction> NodeSet;
/** process build model */
+ virtual void preProcessBuildModel(TheoryModel* m, bool fullModel);
virtual void processBuildModel(TheoryModel* m, bool fullModel);
/** normalize representative */
Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e58c11aca..ffb537734 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -127,7 +127,7 @@ void TheoryUF::check(Effort level) {
throw Exception( ss.str() );
}
//needed for models
- if( options::produceModels() && atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){
+ if( options::produceModels() && ( atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || options::ufssMode()!=UF_SS_FULL ) ){
d_equalityEngine.assertPredicate(atom, polarity, fact);
}
} else {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback