summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-07-12 18:30:15 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-07-12 18:30:15 +0000
commit65798541fa437278cde0c759ab70fd9fa4fe9638 (patch)
tree27341327b8159e58a5ce6371bede6129bf67beb3 /src/theory/quantifiers
parent78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788 (diff)
merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/Makefile.am10
-rw-r--r--src/theory/quantifiers/first_order_model.cpp146
-rw-r--r--src/theory/quantifiers/first_order_model.h82
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp156
-rw-r--r--src/theory/quantifiers/instantiation_engine.h7
-rw-r--r--src/theory/quantifiers/model_engine.cpp1667
-rw-r--r--src/theory/quantifiers/model_engine.h366
-rw-r--r--src/theory/quantifiers/relevant_domain.cpp173
-rw-r--r--src/theory/quantifiers/relevant_domain.h54
-rw-r--r--src/theory/quantifiers/rep_set_iterator.cpp523
-rw-r--r--src/theory/quantifiers/rep_set_iterator.h120
-rw-r--r--src/theory/quantifiers/term_database.cpp324
-rw-r--r--src/theory/quantifiers/term_database.h151
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp27
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h3
-rw-r--r--src/theory/quantifiers/theory_quantifiers_instantiator.cpp2
-rw-r--r--src/theory/quantifiers/theory_quantifiers_instantiator.h2
17 files changed, 2219 insertions, 1594 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index de74e44f8..ae5b99c06 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -16,6 +16,14 @@ libquantifiers_la_SOURCES = \
instantiation_engine.h \
instantiation_engine.cpp \
model_engine.h \
- model_engine.cpp
+ model_engine.cpp \
+ relevant_domain.h \
+ relevant_domain.cpp \
+ rep_set_iterator.h \
+ rep_set_iterator.cpp \
+ term_database.h \
+ term_database.cpp \
+ first_order_model.h \
+ first_order_model.cpp
EXTRA_DIST = kinds \ No newline at end of file
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
new file mode 100644
index 000000000..71a48b33d
--- /dev/null
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -0,0 +1,146 @@
+/********************* */
+/*! \file first_order_model.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 model engine model class
+ **/
+
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/rep_set_iterator.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/uf/theory_uf_strong_solver.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name ),
+d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){
+
+}
+
+void FirstOrderModel::initialize(){
+ //rebuild models
+ d_uf_model.clear();
+ d_array_model.clear();
+ //for each quantifier, collect all operators we care about
+ for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
+ Node f = getAssertedQuantifier( i );
+ //initialize model for term
+ initializeModelForTerm( f[1] );
+ }
+
+ if( Options::current()->printModelEngine ){
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = d_ra.d_type_reps.begin(); it != d_ra.d_type_reps.end(); ++it ){
+ if( uf::StrongSolverTheoryUf::isRelevantType( it->first ) ){
+ Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+ }
+ }
+ }
+}
+
+void FirstOrderModel::initializeModelForTerm( Node n ){
+ if( n.getKind()==APPLY_UF ){
+ Node op = n.getOperator();
+ if( d_uf_model.find( op )==d_uf_model.end() ){
+ TypeNode tn = op.getType();
+ tn = tn[ (int)tn.getNumChildren()-1 ];
+ if( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ){
+ d_uf_model[ op ] = uf::UfModel( op, this );
+ }
+ }
+ }
+ if( n.getKind()!=STORE && n.getType().isArray() ){
+ d_array_model[n] = Node::null();
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ initializeModelForTerm( n[i] );
+ }
+}
+
+void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){
+ if( d_uf_model.find( n )!=d_uf_model.end() ){
+ //d_uf_model[n].toStream( out );
+ Node value = d_uf_model[n].getFunctionValue();
+ out << "(" << n << " " << value << ")";
+ //}else if( d_array_model.find( n )!=d_array_model.end() ){
+ //out << "(" << n << " " << d_array_model[n] << ")" << std::endl;
+ // out << "(" << n << " Array)" << std::endl;
+ }else{
+ DefaultModel::toStreamFunction( n, out );
+ }
+}
+
+void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){
+ DefaultModel::toStreamType( tn, out );
+}
+
+Node FirstOrderModel::getInterpretedValue( TNode n ){
+ Debug("fo-model") << "get interpreted value " << n << std::endl;
+ TypeNode type = n.getType();
+ if( type.isFunction() || type.isPredicate() ){
+ if( d_uf_model.find( n )!=d_uf_model.end() ){
+ return d_uf_model[n].getFunctionValue();
+ }else{
+ return n;
+ }
+ }else if( n.getKind()==APPLY_UF ){
+ int depIndex;
+ return d_uf_model[ n.getOperator() ].getValue( n, depIndex );
+ }
+ return DefaultModel::getInterpretedValue( n );
+}
+
+TermDb* FirstOrderModel::getTermDatabase(){
+ return d_term_db;
+}
+
+
+void FirstOrderModel::toStream(std::ostream& out){
+ DefaultModel::toStream( out );
+#if 0
+ out << "---Current Model---" << std::endl;
+ out << "Representatives: " << std::endl;
+ d_ra.toStream( out );
+ out << "Functions: " << std::endl;
+ for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
+ it->second.toStream( out );
+ out << std::endl;
+ }
+#elif 0
+ d_ra.toStream( out );
+ //print everything not related to UF in equality engine
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ Node eqc = (*eqcs_i);
+ Node rep = getRepresentative( eqc );
+ TypeNode type = rep.getType();
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+ while( !eqc_i.isFinished() ){
+ //do not print things that have interpretations in model
+ if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){
+ out << "(" << (*eqc_i) << " " << rep << ")" << std::endl;
+ }
+ ++eqc_i;
+ }
+ ++eqcs_i;
+ }
+ //print functions
+ for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
+ it->second.toStream( out );
+ out << std::endl;
+ }
+#endif
+} \ No newline at end of file
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
new file mode 100644
index 000000000..832acbee3
--- /dev/null
+++ b/src/theory/quantifiers/first_order_model.h
@@ -0,0 +1,82 @@
+/********************* */
+/*! \file first_order_model.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 Model extended classes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__FIRST_ORDER_MODEL_H
+#define __CVC4__FIRST_ORDER_MODEL_H
+
+#include "theory/model.h"
+#include "theory/uf/theory_uf_model.h"
+
+namespace CVC4 {
+namespace theory {
+
+struct ModelBasisAttributeId {};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+// 0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId {};
+typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
+
+class QuantifiersEngine;
+
+namespace quantifiers{
+
+class TermDb;
+
+class FirstOrderModel : public DefaultModel
+{
+private:
+ //pointer to term database
+ TermDb* d_term_db;
+ //for initialize model
+ void initializeModelForTerm( Node n );
+ /** to stream functions */
+ void toStreamFunction( Node n, std::ostream& out );
+ void toStreamType( TypeNode tn, std::ostream& out );
+public: //for Theory UF:
+ //models for each UF operator
+ std::map< Node, uf::UfModel > d_uf_model;
+public: //for Theory Arrays:
+ //default value for each non-store array
+ std::map< Node, Node > d_array_model;
+public: //for Theory Quantifiers:
+ /** list of quantifiers asserted in the current context */
+ context::CDList<Node> d_forall_asserts;
+ /** get number of asserted quantifiers */
+ int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
+ /** get asserted quantifier */
+ Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
+public:
+ FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );
+ virtual ~FirstOrderModel(){}
+ // initialize the model
+ void initialize();
+ /** get interpreted value */
+ Node getInterpretedValue( TNode n );
+public:
+ /** get term database */
+ TermDb* getTermDatabase();
+ /** to stream function */
+ void toStream( std::ostream& out );
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index c1476acb8..fae54c151 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -18,6 +18,8 @@
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
using namespace std;
using namespace CVC4;
@@ -26,15 +28,9 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-//#define IE_PRINT_PROCESS_TIMES
+InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
+QuantifiersModule( qe ), d_setIncomplete( setIncomplete ){
-InstantiationEngine::InstantiationEngine( TheoryQuantifiers* th ) :
-d_th( th ){
-
-}
-
-QuantifiersEngine* InstantiationEngine::getQuantifiersEngine(){
- return d_th->getQuantifiersEngine();
}
bool InstantiationEngine::hasAddedCbqiLemma( Node f ) {
@@ -46,25 +42,25 @@ void InstantiationEngine::addCbqiLemma( Node f ){
//code for counterexample-based quantifier instantiation
Debug("cbqi") << "Do cbqi for " << f << std::endl;
//make the counterexample body
- //Node ceBody = f[1].substitute( getQuantifiersEngine()->d_vars[f].begin(), getQuantifiersEngine()->d_vars[f].end(),
- // getQuantifiersEngine()->d_inst_constants[f].begin(),
- // getQuantifiersEngine()->d_inst_constants[f].end() );
+ //Node ceBody = f[1].substitute( d_quantEngine->d_vars[f].begin(), d_quantEngine->d_vars[f].end(),
+ // d_quantEngine->d_inst_constants[f].begin(),
+ // d_quantEngine->d_inst_constants[f].end() );
//get the counterexample literal
- Node ceBody = getQuantifiersEngine()->getCounterexampleBody( f );
- Node ceLit = d_th->getValuation().ensureLiteral( ceBody.notNode() );
+ Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
+ Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
d_ce_lit[ f ] = ceLit;
- getQuantifiersEngine()->setInstantiationConstantAttr( ceLit, f );
+ d_quantEngine->getTermDatabase()->setInstantiationConstantAttr( ceLit, f );
// set attributes, mark all literals in the body of n as dependent on cel
//registerLiterals( ceLit, f );
//require any decision on cel to be phase=true
- d_th->getOutputChannel().requirePhase( ceLit, true );
+ d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
//add counterexample lemma
NodeBuilder<> nb(kind::OR);
nb << f << ceLit;
Node lem = nb;
Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
- d_th->getOutputChannel().lemma( lem );
+ d_quantEngine->getOutputChannel().lemma( lem );
}
bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
@@ -72,8 +68,8 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
if( Options::current()->cbqi ){
//check if any cbqi lemma has not been added yet
bool addedLemma = false;
- for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
- Node f = getQuantifiersEngine()->getAssertedQuantifier( i );
+ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
//add cbqi lemma
addCbqiLemma( f );
@@ -87,14 +83,9 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
//if not, proceed to instantiation round
Debug("inst-engine") << "IE: Instantiation Round." << std::endl;
Debug("inst-engine-ctrl") << "IE: Instantiation Round." << std::endl;
- //reset instantiators
+ //reset the quantifiers engine
Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
- for( int i=0; i<theory::THEORY_LAST; i++ ){
- if( getQuantifiersEngine()->getInstantiator( i ) ){
- getQuantifiersEngine()->getInstantiator( i )->resetInstantiationRound( effort );
- }
- }
- getQuantifiersEngine()->getTermDatabase()->reset( effort );
+ d_quantEngine->resetInstantiationRound( effort );
//iterate over an internal effort level e
int e = 0;
int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
@@ -104,20 +95,19 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
d_inst_round_status = InstStrategy::STATUS_SAT;
//instantiate each quantifier
- for( int q=0; q<getQuantifiersEngine()->getNumAssertedQuantifiers(); q++ ){
- Node f = getQuantifiersEngine()->getAssertedQuantifier( q );
+ for( int q=0; q<d_quantEngine->getModel()->getNumAssertedQuantifiers(); q++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( q );
Debug("inst-engine-debug") << "IE: Instantiate " << f << "..." << std::endl;
//if this quantifier is active
- if( getQuantifiersEngine()->getActive( f ) ){
- //int e_use = getQuantifiersEngine()->getRelevance( f )==-1 ? e - 1 : e;
+ if( d_quantEngine->getActive( f ) ){
+ //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e;
int e_use = e;
if( e_use>=0 ){
//use each theory instantiator to instantiate f
for( int i=0; i<theory::THEORY_LAST; i++ ){
- if( getQuantifiersEngine()->getInstantiator( i ) ){
- Debug("inst-engine-debug") << "Do " << getQuantifiersEngine()->getInstantiator( i )->identify() << " " << e_use << std::endl;
- int limitInst = 0;
- int quantStatus = getQuantifiersEngine()->getInstantiator( i )->doInstantiation( f, effort, e_use, limitInst );
+ if( d_quantEngine->getInstantiator( i ) ){
+ Debug("inst-engine-debug") << "Do " << d_quantEngine->getInstantiator( i )->identify() << " " << e_use << std::endl;
+ int quantStatus = d_quantEngine->getInstantiator( i )->doInstantiation( f, effort, e_use );
Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
InstStrategy::updateStatus( d_inst_round_status, quantStatus );
}
@@ -126,31 +116,31 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
}
}
//do not consider another level if already added lemma at this level
- if( getQuantifiersEngine()->hasAddedLemma() ){
+ if( d_quantEngine->hasAddedLemma() ){
d_inst_round_status = InstStrategy::STATUS_UNKNOWN;
}
e++;
}
Debug("inst-engine") << "All instantiators finished, # added lemmas = ";
- Debug("inst-engine") << (int)getQuantifiersEngine()->d_lemmas_waiting.size() << std::endl;
+ Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
//Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
- if( !getQuantifiersEngine()->hasAddedLemma() ){
+ if( !d_quantEngine->hasAddedLemma() ){
Debug("inst-engine-stuck") << "No instantiations produced at this state: " << std::endl;
for( int i=0; i<theory::THEORY_LAST; i++ ){
- if( getQuantifiersEngine()->getInstantiator( i ) ){
- getQuantifiersEngine()->getInstantiator( i )->debugPrint("inst-engine-stuck");
+ if( d_quantEngine->getInstantiator( i ) ){
+ d_quantEngine->getInstantiator( i )->debugPrint("inst-engine-stuck");
Debug("inst-engine-stuck") << std::endl;
}
}
Debug("inst-engine-ctrl") << "---Fail." << std::endl;
return false;
}else{
- Debug("inst-engine-ctrl") << "---Done. " << (int)getQuantifiersEngine()->d_lemmas_waiting.size() << std::endl;
-#ifdef IE_PRINT_PROCESS_TIMES
- Notice() << "lemmas = " << (int)getQuantifiersEngine()->d_lemmas_waiting.size() << std::endl;
-#endif
+ Debug("inst-engine-ctrl") << "---Done. " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
+ if( Options::current()->printInstEngine ){
+ Message() << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
+ }
//flush lemmas to output channel
- getQuantifiersEngine()->flushLemmas( &d_th->getOutputChannel() );
+ d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
return true;
}
}
@@ -174,42 +164,43 @@ void InstantiationEngine::check( Theory::Effort e ){
}
if( performCheck ){
Debug("inst-engine") << "IE: Check " << e << " " << ierCounter << std::endl;
-#ifdef IE_PRINT_PROCESS_TIMES
- double clSet = double(clock())/double(CLOCKS_PER_SEC);
- Notice() << "Run instantiation round " << e << " " << ierCounter << std::endl;
-#endif
+ double clSet = 0;
+ if( Options::current()->printInstEngine ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Message() << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
+ }
bool quantActive = false;
//for each quantifier currently asserted,
// such that the counterexample literal is not in positive in d_counterexample_asserts
// for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) {
// if( (*i).second ) {
- Debug("quantifiers") << "quantifiers: check: asserted quantifiers size"
- << getQuantifiersEngine()->getNumAssertedQuantifiers() << std::endl;
- for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
- Node n = getQuantifiersEngine()->getAssertedQuantifier( i );
+ Debug("quantifiers") << "quantifiers: check: asserted quantifiers size"
+ << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
+ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){
Node cel = d_ce_lit[ n ];
bool active, value;
bool ceValue = false;
- if( d_th->getValuation().hasSatValue( cel, value ) ){
+ if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
active = value;
ceValue = true;
}else{
active = true;
}
- getQuantifiersEngine()->setActive( n, active );
+ d_quantEngine->setActive( n, active );
if( active ){
Debug("quantifiers") << " Active : " << n;
quantActive = true;
}else{
Debug("quantifiers") << " NOT active : " << n;
- if( d_th->getValuation().isDecision( cel ) ){
+ if( d_quantEngine->getValuation().isDecision( cel ) ){
Debug("quant-req-phase") << "Bad decision : " << cel << std::endl;
}
//note that the counterexample literal must not be a decision
- Assert( !d_th->getValuation().isDecision( cel ) );
+ Assert( !d_quantEngine->getValuation().isDecision( cel ) );
}
- if( d_th->getValuation().hasSatValue( n, value ) ){
+ if( d_quantEngine->getValuation().hasSatValue( n, value ) ){
Debug("quantifiers") << ", value = " << value;
}
if( ceValue ){
@@ -217,18 +208,18 @@ void InstantiationEngine::check( Theory::Effort e ){
}
Debug("quantifiers") << std::endl;
}else{
- getQuantifiersEngine()->setActive( n, true );
+ d_quantEngine->setActive( n, true );
quantActive = true;
Debug("quantifiers") << " Active : " << n << ", no ce assigned." << std::endl;
}
Debug("quantifiers-relevance") << "Quantifier : " << n << std::endl;
- Debug("quantifiers-relevance") << " Relevance : " << getQuantifiersEngine()->getRelevance( n ) << std::endl;
- Debug("quantifiers") << " Relevance : " << getQuantifiersEngine()->getRelevance( n ) << std::endl;
+ Debug("quantifiers-relevance") << " Relevance : " << d_quantEngine->getRelevance( n ) << std::endl;
+ Debug("quantifiers") << " Relevance : " << d_quantEngine->getRelevance( n ) << std::endl;
}
//}
if( quantActive ){
bool addedLemmas = doInstantiationRound( e );
- //Debug("quantifiers-dec") << "Do instantiation, level = " << d_th->getValuation().getDecisionLevel() << std::endl;
+ //Debug("quantifiers-dec") << "Do instantiation, level = " << d_quantEngine->getValuation().getDecisionLevel() << std::endl;
//for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
// Debug("quantifiers-dec") << " " << d_valuation.getDecision( i ) << std::endl;
//}
@@ -237,9 +228,12 @@ void InstantiationEngine::check( Theory::Effort e ){
if( d_inst_round_status==InstStrategy::STATUS_SAT ){
Debug("inst-engine") << "No instantiation given, returning SAT..." << std::endl;
debugSat( SAT_INST_STRATEGY );
- }else{
+ }else if( d_setIncomplete ){
Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl;
- d_th->getOutputChannel().setIncomplete();
+ d_quantEngine->getOutputChannel().setIncomplete();
+ }else{
+ Assert( Options::current()->finiteModelFind );
+ Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl;
}
}
}
@@ -250,30 +244,30 @@ void InstantiationEngine::check( Theory::Effort e ){
}
}
}
-#ifdef IE_PRINT_PROCESS_TIMES
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Notice() << "Done Run instantiation round " << (clSet2-clSet) << std::endl;
-#endif
+ if( Options::current()->printInstEngine ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Message() << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
+ }
}
}
void InstantiationEngine::registerQuantifier( Node f ){
//Notice() << "do cbqi " << f << " ? " << std::endl;
- Node ceBody = getQuantifiersEngine()->getCounterexampleBody( f );
+ Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
if( !doCbqi( f ) ){
- getQuantifiersEngine()->addTermToDatabase( ceBody, true );
+ d_quantEngine->addTermToDatabase( ceBody, true );
//need to tell which instantiators will be responsible
//by default, just chose the UF instantiator
- getQuantifiersEngine()->getInstantiator( theory::THEORY_UF )->setHasConstraintsFrom( f );
+ d_quantEngine->getInstantiator( theory::THEORY_UF )->setHasConstraintsFrom( f );
}
//take into account user patterns
if( f.getNumChildren()==3 ){
- Node subsPat = getQuantifiersEngine()->getSubstitutedNode( f[2], f );
+ Node subsPat = d_quantEngine->getTermDatabase()->getSubstitutedNode( f[2], f );
//add patterns
for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
//Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
- ((uf::InstantiatorTheoryUf*)getQuantifiersEngine()->getInstantiator( theory::THEORY_UF ))->addUserPattern( f, subsPat[i] );
+ ((uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( theory::THEORY_UF ))->addUserPattern( f, subsPat[i] );
}
}
}
@@ -337,11 +331,11 @@ bool InstantiationEngine::doCbqi( Node f ){
// registerLiterals( n[i], f );
// }
// if( !d_ce_lit[ f ].isNull() ){
-// if( getQuantifiersEngine()->d_te->getPropEngine()->isSatLiteral( n ) && n.getKind()!=NOT ){
+// if( d_quantEngine->d_te->getPropEngine()->isSatLiteral( n ) && n.getKind()!=NOT ){
// if( n!=d_ce_lit[ f ] && n.notNode()!=d_ce_lit[ f ] ){
// Debug("quant-dep-dec") << "Make " << n << " dependent on ";
// Debug("quant-dep-dec") << d_ce_lit[ f ] << std::endl;
-// d_th->getOutputChannel().dependentDecision( d_ce_lit[ f ], n );
+// d_quantEngine->getOutputChannel().dependentDecision( d_ce_lit[ f ], n );
// }
// }
// }
@@ -351,19 +345,19 @@ bool InstantiationEngine::doCbqi( Node f ){
void InstantiationEngine::debugSat( int reason ){
if( reason==SAT_CBQI ){
//Debug("quantifiers-sat") << "Decisions:" << std::endl;
- //for( int i=1; i<=(int)d_th->getValuation().getDecisionLevel(); i++ ){
- // Debug("quantifiers-sat") << " " << i << ": " << d_th->getValuation().getDecision( i ) << std::endl;
+ //for( int i=1; i<=(int)d_quantEngine->getValuation().getDecisionLevel(); i++ ){
+ // Debug("quantifiers-sat") << " " << i << ": " << d_quantEngine->getValuation().getDecision( i ) << std::endl;
//}
//for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) {
// if( (*i).second ) {
- for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
- Node f = getQuantifiersEngine()->getAssertedQuantifier( i );
+ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
Node cel = d_ce_lit[ f ];
Assert( !cel.isNull() );
bool value;
- if( d_th->getValuation().hasSatValue( cel, value ) ){
+ if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
if( !value ){
- AlwaysAssert(! d_th->getValuation().isDecision( cel ),
+ AlwaysAssert(! d_quantEngine->getValuation().isDecision( cel ),
"bad decision on counterexample literal");
}
}
@@ -386,9 +380,9 @@ void InstantiationEngine::propagate( Theory::Effort level ){
//propagate as decision all counterexample literals that are not asserted
for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){
bool value;
- if( !d_th->getValuation().hasSatValue( it->second, value ) ){
+ if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){
//if not already set, propagate as decision
- d_th->getOutputChannel().propagateAsDecision( it->second );
+ d_quantEngine->getOutputChannel().propagateAsDecision( it->second );
Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl;
}
}
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index c6aaed18a..13de210ab 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -29,14 +29,13 @@ namespace quantifiers {
class InstantiationEngine : public QuantifiersModule
{
private:
- TheoryQuantifiers* d_th;
- QuantifiersEngine* getQuantifiersEngine();
-private:
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
/** status of instantiation round (one of InstStrategy::STATUS_*) */
int d_inst_round_status;
/** map from universal quantifiers to their counterexample literals */
std::map< Node, Node > d_ce_lit;
+ /** whether the instantiation engine should set incomplete if it cannot answer SAT */
+ bool d_setIncomplete;
private:
bool hasAddedCbqiLemma( Node f );
void addCbqiLemma( Node f );
@@ -59,7 +58,7 @@ private:
/** debug sat */
void debugSat( int reason );
public:
- InstantiationEngine( TheoryQuantifiers* th );
+ InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
~InstantiationEngine(){}
void check( Theory::Effort e );
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index a72b103d1..ad259f864 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -15,19 +15,23 @@
**/
#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/rep_set_iterator.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
-//#define ME_PRINT_PROCESS_TIMES
+//#define ME_PRINT_WARNINGS
//#define DISABLE_EVAL_SKIP_MULTIPLE
-#define RECONSIDER_FUNC_DEFAULT_VALUE
+
#define RECONSIDER_FUNC_CONSTANT
-#define USE_INDEX_ORDERING
-//#define ONE_INST_PER_QUANT_PER_ROUND
+#define EVAL_FAIL_SKIP_MULTIPLE
+//#define ONE_QUANT_PER_ROUND_INST_GEN
+//#define ONE_QUANT_PER_ROUND
using namespace std;
using namespace CVC4;
@@ -36,570 +40,417 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-void printRepresentative( const char* c, QuantifiersEngine* qe, Node r ){
- if( r.getType()==NodeManager::currentNM()->booleanType() ){
- if( qe->getEqualityQuery()->areEqual( r, NodeManager::currentNM()->mkConst( true ) ) ){
- Debug( c ) << "true";
- }else{
- Debug( c ) << "false";
- }
- }else{
- Debug( c ) << qe->getEqualityQuery()->getRepresentative( r );
- }
-}
-
-RepAlphabet::RepAlphabet( RepAlphabet& ra, QuantifiersEngine* qe ){
- //translate to current representatives
- for( std::map< TypeNode, std::vector< Node > >::iterator it = ra.d_type_reps.begin(); it != ra.d_type_reps.end(); ++it ){
- std::vector< Node > reps;
- for( int i=0; i<(int)it->second.size(); i++ ){
- //reps.push_back( ie->getEqualityQuery()->getRepresentative( it->second[i] ) );
- reps.push_back( it->second[i] );
- }
- set( it->first, reps );
- }
-}
-
-void RepAlphabet::set( TypeNode t, std::vector< Node >& reps ){
- d_type_reps[t].insert( d_type_reps[t].begin(), reps.begin(), reps.end() );
- for( int i=0; i<(int)reps.size(); i++ ){
- d_tmap[ reps[i] ] = i;
- }
-}
-
-void RepAlphabet::debugPrint( const char* c, QuantifiersEngine* qe ){
- for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
- Debug( c ) << it->first << " : " << std::endl;
- for( int i=0; i<(int)it->second.size(); i++ ){
- Debug( c ) << " " << i << ": " << it->second[i] << std::endl;
- Debug( c ) << " eq_class( " << it->second[i] << " ) : ";
- ((uf::InstantiatorTheoryUf*)qe->getInstantiator( THEORY_UF ))->outputEqClass( c, it->second[i] );
- Debug( c ) << std::endl;
- }
- }
-}
-
-RepAlphabetIterator::RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model ){
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- d_index_order.push_back( i );
- }
- initialize( qe, f, model );
-}
-
-RepAlphabetIterator::RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model, std::vector< int >& indexOrder ){
- d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
- initialize( qe, f, model );
-}
-
-void RepAlphabetIterator::initialize( QuantifiersEngine* qe, Node f, ModelEngine* model ){
- d_f = f;
- d_model = model;
- //store instantiation constants
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- d_ic.push_back( qe->getInstantiationConstant( d_f, i ) );
- d_index.push_back( 0 );
- }
- //make the d_var_order mapping
- for( size_t i=0; i<d_index_order.size(); i++ ){
- d_var_order[d_index_order[i]] = i;
- }
- //for testing
- d_inst_tried = 0;
- d_inst_tests = 0;
-}
-
-void RepAlphabetIterator::increment2( QuantifiersEngine* qe, int counter ){
- Assert( !isFinished() );
- //increment d_index
- while( counter>=0 && d_index[counter]==(int)(d_model->getReps()->d_type_reps[d_f[0][d_index_order[counter]].getType()].size()-1) ){
- counter--;
- }
- if( counter==-1 ){
- d_index.clear();
- }else{
- for( int i=(int)d_index.size()-1; i>counter; i-- ){
- d_index[i] = 0;
- d_model->clearEvalFailed( i );
- }
- d_index[counter]++;
- d_model->clearEvalFailed( counter );
- }
-}
-
-void RepAlphabetIterator::increment( QuantifiersEngine* qe ){
- if( !isFinished() ){
- increment2( qe, (int)d_index.size()-1 );
- }
-}
+ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) :
+TheoryEngineModelBuilder( qe->getTheoryEngine() ),
+d_qe( qe ){
-bool RepAlphabetIterator::isFinished(){
- return d_index.empty();
}
-void RepAlphabetIterator::getMatch( QuantifiersEngine* ie, InstMatch& m ){
- for( int i=0; i<(int)d_index.size(); i++ ){
- m.d_map[ ie->getInstantiationConstant( d_f, i ) ] = getTerm( i );
- }
+Node ModelEngineBuilder::chooseRepresentative( TheoryModel* tm, Node eqc ){
+ return eqc;
}
-Node RepAlphabetIterator::getTerm( int i ){
- TypeNode tn = d_f[0][d_index_order[i]].getType();
- Assert( d_model->getReps()->d_type_reps.find( tn )!=d_model->getReps()->d_type_reps.end() );
- return d_model->getReps()->d_type_reps[tn][d_index[d_index_order[i]]];
-}
-
-void RepAlphabetIterator::calculateTerms( QuantifiersEngine* qe ){
- d_terms.clear();
- for( int i=0; i<qe->getNumInstantiationConstants( d_f ); i++ ){
- d_terms.push_back( getTerm( i ) );
- }
-}
-
-void RepAlphabetIterator::debugPrint( const char* c ){
- for( int i=0; i<(int)d_index.size(); i++ ){
- Debug( c ) << i << ": " << d_index[i] << ", (" << getTerm( i ) << " / " << d_ic[ i ] << std::endl;
- }
-}
-
-void RepAlphabetIterator::debugPrintSmall( const char* c ){
- Debug( c ) << "RI: ";
- for( int i=0; i<(int)d_index.size(); i++ ){
- Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
- }
- Debug( c ) << std::endl;
-}
-
-//set value function
-void UfModelTree::setValue( QuantifiersEngine* qe, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
- if( d_data.empty() ){
- d_value = v;
- }else if( !d_value.isNull() && d_value!=v ){
- d_value = Node::null();
- }
- if( argIndex<(int)n.getNumChildren() ){
- //take r = null when argument is the model basis
- Node r;
- if( ground || !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ){
- r = qe->getEqualityQuery()->getRepresentative( n[ indexOrder[argIndex] ] );
- }
- d_data[ r ].setValue( qe, n, v, indexOrder, ground, argIndex+1 );
- }
-}
-
-//get value function
-Node UfModelTree::getValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){
- if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){
- //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;
- depIndex = argIndex;
- return d_value;
- }else{
- Node val;
- int childDepIndex[2] = { argIndex, argIndex };
- for( int i=0; i<2; i++ ){
- //first check the argument, then check default
- Node r;
- if( i==0 ){
- r = qe->getEqualityQuery()->getRepresentative( n[ indexOrder[argIndex] ] );
+void ModelEngineBuilder::processBuildModel( TheoryModel* m ) {
+ d_addedLemmas = 0;
+ //only construct first order model if optUseModel() is true
+ if( optUseModel() ){
+ FirstOrderModel* fm = (FirstOrderModel*)m;
+ //initialize model
+ fm->initialize();
+ //analyze the quantifiers
+ Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl;
+ analyzeQuantifiers( fm );
+ //if applicable, find exceptions
+ if( optInstGen() ){
+ //now, see if we know that any exceptions via InstGen exist
+ Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ if( d_quant_sat.find( f )==d_quant_sat.end() ){
+ d_addedLemmas += doInstGen( fm, f );
+ if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
+ break;
+ }
+ }
}
- std::map< Node, UfModelTree >::iterator it = d_data.find( r );
- if( it!=d_data.end() ){
- val = it->second.getValue( qe, n, indexOrder, childDepIndex[i], argIndex+1 );
- if( !val.isNull() ){
- break;
+ if( Options::current()->printModelEngine ){
+ if( d_addedLemmas>0 ){
+ Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+ }else{
+ Message() << "No InstGen lemmas..." << std::endl;
}
- }else{
- //argument is not a defined argument: thus, it depends on this argument
- childDepIndex[i] = argIndex+1;
}
+ Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl;
+ }
+ if( d_addedLemmas==0 ){
+ //if no immediate exceptions, build the model
+ // this model will be an approximation that will need to be tested via exhaustive instantiation
+ Debug("fmf-model-debug") << "Building model..." << std::endl;
+ finishBuildModel( fm );
}
- //update depIndex
- depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];
- //Notice() << "Return " << val << ", depIndex = " << depIndex;
- //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;
- return val;
}
}
-//simplify function
-void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){
- if( argIndex<(int)op.getType().getNumChildren()-1 ){
- std::vector< Node > eraseData;
- //first process the default argument
- Node r;
- std::map< Node, UfModelTree >::iterator it = d_data.find( r );
- if( it!=d_data.end() ){
- if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
- eraseData.push_back( r );
- }else{
- it->second.simplify( op, defaultVal, argIndex+1 );
- if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
- defaultVal = it->second.d_value;
+void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){
+ d_quant_selection_lits.clear();
+ d_quant_sat.clear();
+ d_uf_prefs.clear();
+ int quantSatInit = 0;
+ int nquantSatInit = 0;
+ //analyze the preferences of each quantifier
+ for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
+ std::vector< Node > pro_con[2];
+ std::vector< Node > constantSatOps;
+ bool constantSatReconsider;
+ //for each asserted quantifier f,
+ // - determine which literals form model basis for each quantifier
+ // - check which function/predicates have good and bad definitions according to f
+ for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
+ it != d_qe->d_phase_reqs[f].end(); ++it ){
+ Node n = it->first;
+ Node gn = d_qe->getTermDatabase()->getModelBasis( n );
+ Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl;
+ //calculate preference
+ int pref = 0;
+ bool value;
+ if( d_qe->getValuation().hasSatValue( gn, value ) ){
+ if( value!=it->second ){
+ //store this literal as a model basis literal
+ // this literal will force a default values in model that (modulo exceptions) shows
+ // that f is satisfied by the model
+ d_quant_selection_lits[f].push_back( value ? n : n.notNode() );
+ pref = 1;
}else{
- defaultVal = Node::null();
+ pref = -1;
}
}
- }
- //now see if any children can be removed, and simplify the ones that cannot
- for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
- if( !it->first.isNull() ){
- if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
- eraseData.push_back( it->first );
+ if( pref!=0 ){
+ //Store preferences for UF
+ bool isConst = !n.hasAttribute(InstConstantAttribute());
+ std::vector< Node > uf_terms;
+ if( gn.getKind()==APPLY_UF ){
+ uf_terms.push_back( gn );
+ isConst = fm->d_uf_model[gn.getOperator()].isConstant();
+ }else if( gn.getKind()==EQUAL ){
+ isConst = true;
+ for( int j=0; j<2; j++ ){
+ if( n[j].hasAttribute(InstConstantAttribute()) ){
+ if( n[j].getKind()==APPLY_UF ){
+ Node op = gn[j].getOperator();
+ if( fm->d_uf_model.find( op )!=fm->d_uf_model.end() ){
+ uf_terms.push_back( gn[j] );
+ isConst = isConst && fm->d_uf_model[op].isConstant();
+ }else{
+ isConst = false;
+ }
+ }else{
+ isConst = false;
+ }
+ }
+ }
+ }
+ Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" );
+ Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
+ if( pref==1 && isConst ){
+ d_quant_sat[f] = true;
+ //instead, just note to the model for each uf term that f is pro its definition
+ constantSatReconsider = false;
+ constantSatOps.clear();
+ for( int j=0; j<(int)uf_terms.size(); j++ ){
+ Node op = uf_terms[j].getOperator();
+ constantSatOps.push_back( op );
+ if( d_uf_prefs[op].d_reconsiderModel ){
+ constantSatReconsider = true;
+ }
+ }
+ if( !constantSatReconsider ){
+ break;
+ }
}else{
- it->second.simplify( op, defaultVal, argIndex+1 );
+ int pcIndex = pref==1 ? 0 : 1;
+ for( int j=0; j<(int)uf_terms.size(); j++ ){
+ pro_con[pcIndex].push_back( uf_terms[j] );
+ }
}
}
}
- for( int i=0; i<(int)eraseData.size(); i++ ){
- d_data.erase( eraseData[i] );
- }
- }
-}
-
-//is total function
-bool UfModelTree::isTotal( Node op, int argIndex ){
- if( argIndex==(int)(op.getType().getNumChildren()-1) ){
- return !d_value.isNull();
- }else{
- Node r;
- std::map< Node, UfModelTree >::iterator it = d_data.find( r );
- if( it!=d_data.end() ){
- return it->second.isTotal( op, argIndex+1 );
+ if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+ Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: ";
+ for( int i=0; i<(int)constantSatOps.size(); i++ ){
+ Debug("fmf-model-prefs") << constantSatOps[i] << " ";
+ d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false;
+ }
+ Debug("fmf-model-prefs") << std::endl;
+ quantSatInit++;
+ d_statistics.d_pre_sat_quant += quantSatInit;
}else{
- return false;
- }
- }
-}
-
-Node UfModelTree::getConstantValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int argIndex ){
- return d_value;
-}
-
-void indent( const char* c, int ind ){
- for( int i=0; i<ind; i++ ){
- Debug( c ) << " ";
- }
-}
-
-void UfModelTree::debugPrint( const char* c, QuantifiersEngine* qe, std::vector< int >& indexOrder, int ind, int arg ){
- if( !d_data.empty() ){
- for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
- if( !it->first.isNull() ){
- indent( c, ind );
- Debug( c ) << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
- it->second.debugPrint( c, qe, indexOrder, ind+2, arg+1 );
+ nquantSatInit++;
+ d_statistics.d_pre_nsat_quant += quantSatInit;
+ //note quantifier's value preferences to models
+ for( int k=0; k<2; k++ ){
+ for( int j=0; j<(int)pro_con[k].size(); j++ ){
+ Node op = pro_con[k][j].getOperator();
+ Node r = fm->getRepresentative( pro_con[k][j] );
+ d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+ }
}
}
- if( d_data.find( Node::null() )!=d_data.end() ){
- d_data[ Node::null() ].debugPrint( c, qe, indexOrder, ind, arg+1 );
- }
- }else{
- indent( c, ind );
- Debug( c ) << "return ";
- printRepresentative( c, qe, d_value );
- //Debug( c ) << " { ";
- //for( int i=0; i<(int)d_explicit.size(); i++ ){
- // Debug( c ) << d_explicit[i] << " ";
- //}
- //Debug( c ) << "}";
- Debug( c ) << std::endl;
}
+ Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
}
-UfModel::UfModel( Node op, ModelEngine* me ) : d_op( op ), d_me( me ),
- d_model_constructed( false ), d_reconsider_model( false ){
-
- d_tree = UfModelTreeOrdered( op ); TypeNode tn = d_op.getType(); tn = tn[(int)tn.getNumChildren()-1]; Assert( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ); //look at ground assertions
- for( int i=0; i<(int)d_me->getQuantifiersEngine()->getTermDatabase()->d_op_map[ d_op ].size(); i++ ){
- Node n = d_me->getQuantifiersEngine()->getTermDatabase()->d_op_map[ d_op ][i];
- bool add = true;
- if( n.getAttribute(NoMatchAttribute()) ){
- add = false;
- //determine if it has model basis attribute
- for( int j=0; j<(int)n.getNumChildren(); j++ ){
- if( n[j].getAttribute(ModelBasisAttribute()) ){
- add = true;
- break;
+int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){
+ //we wish to add all known exceptions to our model basis literal(s)
+ // this will help to refine our current model.
+ //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
+ // effectively acting as partial instantiations instead of pointwise instantiations.
+ int addedLemmas = 0;
+ for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){
+ bool phase = d_quant_selection_lits[f][i].getKind()!=NOT;
+ Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i];
+ Assert( lit.hasAttribute(InstConstantAttribute()) );
+ std::vector< Node > tr_terms;
+ if( lit.getKind()==APPLY_UF ){
+ //only match predicates that are contrary to this one, use literal matching
+ Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
+ fm->getTermDatabase()->setInstantiationConstantAttr( eq, f );
+ tr_terms.push_back( eq );
+ }else if( lit.getKind()==EQUAL ){
+ //collect trigger terms
+ for( int j=0; j<2; j++ ){
+ if( lit[j].hasAttribute(InstConstantAttribute()) ){
+ if( lit[j].getKind()==APPLY_UF ){
+ tr_terms.push_back( lit[j] );
+ }else{
+ tr_terms.clear();
+ break;
+ }
}
}
- }
- if( add ){
- d_ground_asserts.push_back( n );
- Node r = d_me->getQuantifiersEngine()->getEqualityQuery()->getRepresentative( n );
- d_ground_asserts_reps.push_back( r );
- }
- }
- //determine if it is constant
- if( !d_ground_asserts.empty() ){
- bool isConstant = true;
- for( int i=1; i<(int)d_ground_asserts.size(); i++ ){
- if( d_ground_asserts_reps[0]!=d_ground_asserts_reps[i] ){
- isConstant = false;
- break;
+ if( tr_terms.size()==1 && !phase ){
+ //equality between a function and a ground term, use literal matching
+ tr_terms.clear();
+ tr_terms.push_back( lit );
}
}
- if( isConstant ){
- //set constant value
- Node t = d_me->getModelBasisApplyUfTerm( d_op );
- Node r = d_ground_asserts_reps[0];
- setValue( t, r, false );
- setModel();
- d_reconsider_model = true;
- Debug("fmf-model-cons") << "Function " << d_op << " is the constant function ";
- printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), r );
- Debug("fmf-model-cons") << std::endl;
+ //if applicable, try to add exceptions here
+ if( !tr_terms.empty() ){
+ //make a trigger for these terms, add instantiations
+ Trigger* tr = Trigger::mkTrigger( d_qe, f, tr_terms );
+ //Notice() << "Trigger = " << (*tr) << std::endl;
+ tr->resetInstantiationRound();
+ tr->reset( Node::null() );
+ //d_qe->d_optInstMakeRepresentative = false;
+ //d_qe->d_optMatchIgnoreModelBasis = true;
+ addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
}
}
+ return addedLemmas;
}
-void UfModel::setValue( Node n, Node v, bool ground ){
- d_set_values[ ground ? 1 : 0 ][n] = v;
-}
-
-void UfModel::setModel(){
- makeModel( d_me->getQuantifiersEngine(), d_tree );
- d_model_constructed = true;
-}
-
-void UfModel::clearModel(){
- for( int k=0; k<2; k++ ){
- d_set_values[k].clear();
+void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){
+ //build model for UF
+ for( std::map< Node, uf::UfModel >::iterator it = fm->d_uf_model.begin(); it != fm->d_uf_model.end(); ++it ){
+ finishBuildModelUf( fm, it->second );
}
- d_tree.clear();
- d_model_constructed = false;
-}
-
-Node UfModel::getConstantValue( QuantifiersEngine* qe, Node n ){
- if( d_model_constructed ){
- return d_tree.getConstantValue( qe, n );
- }else{
- return Node::null();
+ //build model for arrays
+ for( std::map< Node, Node >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){
+ //consult the model basis select term
+ // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term
+ TypeNode tn = it->first.getType();
+ Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) );
+ it->second = fm->getRepresentative( selModelBasis );
}
+ Debug("fmf-model-debug") << "Done building models." << std::endl;
}
-bool UfModel::isConstant(){
- Node gn = d_me->getModelBasisApplyUfTerm( d_op );
- Node n = getConstantValue( d_me->getQuantifiersEngine(), gn );
- return !n.isNull();
-}
-
-void UfModel::buildModel(){
+void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ){
+ Node op = model.getOperator();
#ifdef RECONSIDER_FUNC_CONSTANT
- if( d_model_constructed ){
- if( d_reconsider_model ){
+ if( model.isModelConstructed() && model.isConstant() ){
+ if( d_uf_prefs[op].d_reconsiderModel ){
//if we are allowed to reconsider default value, then see if the default value can be improved
- Node t = d_me->getModelBasisApplyUfTerm( d_op );
- Node v = d_set_values[0][t];
- if( d_value_pro_con[1][v].size()>d_value_pro_con[0][v].size() ){
- Debug("fmf-model-cons-debug") << "Consider changing the default value for " << d_op << std::endl;
- clearModel();
+ Node t = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
+ Node v = model.getConstantValue( t );
+ if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
+ Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
+ model.clearModel();
}
}
}
#endif
- //now, construct models for each uninterpretted function/predicate
- if( !d_model_constructed ){
- Debug("fmf-model-cons") << "Construct model for " << d_op << "..." << std::endl;
- //now, set the values in the model
- for( int i=0; i<(int)d_ground_asserts.size(); i++ ){
- Node n = d_ground_asserts[i];
- Node v = d_ground_asserts_reps[i];
+ if( !model.isModelConstructed() ){
+ //construct the model for the uninterpretted function/predicate
+ bool setDefaultVal = true;
+ Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
+ Debug("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
+ //set the values in the model
+ for( size_t i=0; i<model.d_ground_asserts.size(); i++ ){
+ Node n = model.d_ground_asserts[i];
+ Node v = model.d_ground_asserts_reps[i];
//if this assertion did not help the model, just consider it ground
//set n = v in the model tree
Debug("fmf-model-cons") << " Set " << n << " = ";
- printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), v );
+ fm->printRepresentativeDebug( "fmf-model-cons", v );
Debug("fmf-model-cons") << std::endl;
//set it as ground value
- setValue( n, v );
- }
- //set the default value
- //chose defaultVal based on heuristic (the best proportion of "pro" responses)
- Node defaultVal;
- double maxScore = -1;
- for( int i=0; i<(int)d_values.size(); i++ ){
- Node v = d_values[i];
- double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() );
- Debug("fmf-model-cons") << " - score( ";
- printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), v );
- Debug("fmf-model-cons") << " ) = " << score << std::endl;
- if( score>maxScore ){
- defaultVal = v;
- maxScore = score;
- }
- }
-#ifdef RECONSIDER_FUNC_DEFAULT_VALUE
- if( maxScore<1.0 ){
- //consider finding another value, if possible
- Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;
- TypeNode tn = d_op.getType();
- Node newDefaultVal = d_me->getArbitraryElement( tn[(int)tn.getNumChildren()-1], d_values );
- if( !newDefaultVal.isNull() ){
- defaultVal = newDefaultVal;
- Debug("fmf-model-cons-debug") << "-> Change default value to ";
- printRepresentative( "fmf-model-cons-debug", d_me->getQuantifiersEngine(), defaultVal );
- Debug("fmf-model-cons-debug") << std::endl;
+ model.setValue( n, v );
+ if( model.optUsePartialDefaults() ){
+ //also set as default value if necessary
+ //if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){
+ if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){
+ model.setValue( n, v, false );
+ if( n==defaultTerm ){
+ //incidentally already set, we will not need to find a default value
+ setDefaultVal = false;
+ }
+ }
}else{
- Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl;
- Debug("fmf-model-cons-debug") << " Excluding: ";
- for( int i=0; i<(int)d_values.size(); i++ ){
- Debug("fmf-model-cons-debug") << d_values[i] << " ";
+ if( n==defaultTerm ){
+ model.setValue( n, v, false );
+ //incidentally already set, we will not need to find a default value
+ setDefaultVal = false;
}
- Debug("fmf-model-cons-debug") << std::endl;
}
}
-#endif
- Assert( !defaultVal.isNull() );
- //get the default term (this term must be defined non-ground in model)
- Node defaultTerm = d_me->getModelBasisApplyUfTerm( d_op );
- Debug("fmf-model-cons") << " Choose ";
- printRepresentative("fmf-model-cons", d_me->getQuantifiersEngine(), defaultVal );
- Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl;
- Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;
- Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;
- setValue( defaultTerm, defaultVal, false );
+ //set the overall default value if not set already (is this necessary??)
+ if( setDefaultVal ){
+ Debug("fmf-model-cons") << " Choose default value..." << std::endl;
+ //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
+ Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
+ Assert( !defaultVal.isNull() );
+ model.setValue( defaultTerm, defaultVal, false );
+ }
Debug("fmf-model-cons") << " Making model...";
- setModel();
- Debug("fmf-model-cons") << " Finished constructing model for " << d_op << "." << std::endl;
+ model.setModel();
+ Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl;
}
}
-void UfModel::setValuePreference( Node f, Node n, bool isPro ){
- Node v = d_me->getQuantifiersEngine()->getEqualityQuery()->getRepresentative( n );
- //Notice() << "Set value preference " << n << " = " << v << " " << isPro << std::endl;
- if( std::find( d_values.begin(), d_values.end(), v )==d_values.end() ){
- d_values.push_back( v );
- }
- int index = isPro ? 0 : 1;
- if( std::find( d_value_pro_con[index][v].begin(), d_value_pro_con[index][v].end(), f )==d_value_pro_con[index][v].end() ){
- d_value_pro_con[index][v].push_back( f );
- }
+bool ModelEngineBuilder::optUseModel() {
+ return Options::current()->fmfModelBasedInst;
}
-void UfModel::makeModel( QuantifiersEngine* qe, UfModelTreeOrdered& tree ){
- for( int k=0; k<2; k++ ){
- for( std::map< Node, Node >::iterator it = d_set_values[k].begin(); it != d_set_values[k].end(); ++it ){
- tree.setValue( qe, it->first, it->second, k==1 );
- }
- }
- tree.simplify();
+bool ModelEngineBuilder::optInstGen(){
+ return Options::current()->fmfInstGen;
+}
+
+bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
+#ifdef ONE_QUANT_PER_ROUND_INST_GEN
+ return true;
+#else
+ return false;
+#endif
}
-void UfModel::debugPrint( const char* c ){
- //Debug( c ) << "Function " << d_op << std::endl;
- //Debug( c ) << " Type: " << d_op.getType() << std::endl;
- //Debug( c ) << " Ground asserts:" << std::endl;
- //for( int i=0; i<(int)d_ground_asserts.size(); i++ ){
- // Debug( c ) << " " << d_ground_asserts[i] << " = ";
- // printRepresentative( c, d_me->getQuantifiersEngine(), d_ground_asserts[i] );
- // Debug( c ) << std::endl;
- //}
- //Debug( c ) << " Model:" << std::endl;
+ModelEngineBuilder::Statistics::Statistics():
+ d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0),
+ d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0)
+{
+ StatisticsRegistry::registerStat(&d_pre_sat_quant);
+ StatisticsRegistry::registerStat(&d_pre_nsat_quant);
+}
- TypeNode t = d_op.getType();
- Debug( c ) << d_op << "( ";
- for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){
- Debug( c ) << "x_" << i << " : " << t[i];
- if( i<(int)(t.getNumChildren()-2) ){
- Debug( c ) << ", ";
- }
- }
- Debug( c ) << " ) : " << t[(int)t.getNumChildren()-1] << std::endl;
- if( d_tree.isEmpty() ){
- Debug( c ) << " [undefined]" << std::endl;
- }else{
- d_tree.debugPrint( c, d_me->getQuantifiersEngine(), 3 );
- Debug( c ) << std::endl;
- }
- //Debug( c ) << " Phase reqs:" << std::endl; //for( int i=0; i<2; i++ ){
- // for( std::map< Node, std::vector< Node > >::iterator it = d_reqs[i].begin(); it != d_reqs[i].end(); ++it ){
- // Debug( c ) << " " << it->first << std::endl;
- // for( int j=0; j<(int)it->second.size(); j++ ){
- // Debug( c ) << " " << it->second[j] << " -> " << (i==1) << std::endl;
- // }
- // }
- //}
- //Debug( c ) << std::endl;
- //for( int i=0; i<2; i++ ){
- // for( std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_eq_reqs[i].begin(); it != d_eq_reqs[i].end(); ++it ){
- // Debug( c ) << " " << "For " << it->first << ":" << std::endl;
- // for( std::map< Node, std::vector< Node > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- // for( int j=0; j<(int)it2->second.size(); j++ ){
- // Debug( c ) << " " << it2->first << ( i==1 ? "==" : "!=" ) << it2->second[j] << std::endl;
- // }
- // }
- // }
- //}
+ModelEngineBuilder::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
+ StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
}
//Model Engine constructor
-ModelEngine::ModelEngine( TheoryQuantifiers* th ){
- d_th = th;
- d_quantEngine = th->getQuantifiersEngine();
- d_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getStrongSolver();
+ModelEngine::ModelEngine( QuantifiersEngine* qe ) :
+QuantifiersModule( qe ),
+d_builder( qe ),
+d_rel_domain( qe->getModel() ){
+
}
void ModelEngine::check( Theory::Effort e ){
- if( e==Theory::EFFORT_LAST_CALL ){
- bool quantsInit = true;
+ if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
//first, check if we can minimize the model further
- if( !d_ss->minimize() ){
+ if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getStrongSolver()->minimize() ){
return;
}
- if( useModel() ){
- //now, check if any quantifiers are un-initialized
- for( int i=0; i<d_quantEngine->getNumAssertedQuantifiers(); i++ ){
- Node f = d_quantEngine->getAssertedQuantifier( i );
- if( !initializeQuantifier( f ) ){
- quantsInit = false;
- }
+ //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
+ int addedLemmas = 0;
+ if( d_builder.optUseModel() ){
+ //check if any quantifiers are un-initialized
+ for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ addedLemmas += initializeQuantifier( f );
}
}
- if( quantsInit ){
-#ifdef ME_PRINT_PROCESS_TIMES
- Notice() << "---Instantiation Round---" << std::endl;
-#endif
+ if( addedLemmas==0 ){
+ //quantifiers are initialized, we begin an instantiation round
+ double clSet = 0;
+ if( Options::current()->printModelEngine ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Message() << "---Model Engine Round---" << std::endl;
+ }
Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl;
++(d_statistics.d_inst_rounds);
- d_quantEngine->getTermDatabase()->reset( e );
- //build the representatives
- Debug("fmf-model-debug") << "Building representatives..." << std::endl;
- buildRepresentatives();
- if( useModel() ){
- //initialize the model
- Debug("fmf-model-debug") << "Initializing model..." << std::endl;
- initializeModel();
- //analyze the quantifiers
- Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl;
- analyzeQuantifiers();
- //build the model
- Debug("fmf-model-debug") << "Building model..." << std::endl;
- for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
- it->second.buildModel();
+ //reset the quantifiers engine
+ d_quantEngine->resetInstantiationRound( e );
+ //initialize the model
+ Debug("fmf-model-debug") << "Build model..." << std::endl;
+ d_builder.buildModel( d_quantEngine->getModel() );
+ d_quantEngine->d_model_set = true;
+ //if builder has lemmas, add and return
+ if( d_builder.d_addedLemmas>0 ){
+ addedLemmas += (int)d_builder.d_addedLemmas;
+ }else{
+ //print debug
+ Debug("fmf-model-complete") << std::endl;
+ debugPrint("fmf-model-complete");
+ //verify we are SAT by trying exhaustive instantiation
+ if( optUseRelevantDomain() ){
+ d_rel_domain.compute();
}
- }
- //print debug
- debugPrint("fmf-model-complete");
- //try exhaustive instantiation
- Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
- int addedLemmas = 0;
- for( int i=0; i<d_quantEngine->getNumAssertedQuantifiers(); i++ ){
- Node f = d_quantEngine->getAssertedQuantifier( i );
- if( d_quant_sat.find( f )==d_quant_sat.end() ){
- addedLemmas += instantiateQuantifier( f );
+ d_triedLemmas = 0;
+ d_testLemmas = 0;
+ d_relevantLemmas = 0;
+ d_totalLemmas = 0;
+ Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
+ for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ if( d_builder.d_quant_sat.find( f )==d_builder.d_quant_sat.end() ){
+ addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
+ if( optOneQuantPerRound() && addedLemmas>0 ){
+ break;
+ }
+ }
+#ifdef ME_PRINT_WARNINGS
+ if( addedLemmas>10000 ){
+ break;
+ }
+#endif
+ }
+ Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+ Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+ if( Options::current()->printModelEngine ){
+ Message() << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+ Message() << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Message() << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+ }
+#ifdef ME_PRINT_WARNINGS
+ if( addedLemmas>10000 ){
+ Debug("fmf-exit") << std::endl;
+ debugPrint("fmf-exit");
+ exit( 0 );
}
- }
-#ifdef ME_PRINT_PROCESS_TIMES
- Notice() << "Added Lemmas = " << addedLemmas << std::endl;
#endif
- if( addedLemmas==0 ){
- //debugPrint("fmf-consistent");
- //for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
- // it->second.simplify();
- //}
- Debug("fmf-consistent") << std::endl;
- debugPrint("fmf-consistent");
}
}
- d_quantEngine->flushLemmas( &d_th->getOutputChannel() );
+ if( addedLemmas==0 ){
+ //CVC4 will answer SAT
+ Debug("fmf-consistent") << std::endl;
+ debugPrint("fmf-consistent");
+ }else{
+ //otherwise, the search will continue
+ d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
+ }
}
}
@@ -611,19 +462,31 @@ void ModelEngine::assertNode( Node f ){
}
-bool ModelEngine::useModel() {
- return Options::current()->fmfModelBasedInst;
+bool ModelEngine::optOneInstPerQuantRound(){
+ return Options::current()->fmfOneInstPerRound;
+}
+
+bool ModelEngine::optUseRelevantDomain(){
+ return Options::current()->fmfRelevantDomain;
+}
+
+bool ModelEngine::optOneQuantPerRound(){
+#ifdef ONE_QUANT_PER_ROUND
+ return true;
+#else
+ return false;
+#endif
}
-bool ModelEngine::initializeQuantifier( Node f ){
+int ModelEngine::initializeQuantifier( Node f ){
if( d_quant_init.find( f )==d_quant_init.end() ){
d_quant_init[f] = true;
Debug("inst-fmf-init") << "Initialize " << f << std::endl;
//add the model basis instantiation
// This will help produce the necessary information for model completion.
- // We do this by extending distinguish ground assertions (those
+ // We do this by extending distinguish ground assertions (those
// containing terms with "model basis" attribute) to hold for all cases.
-
+
////first, check if any variables are required to be equal
//for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
// it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
@@ -632,747 +495,167 @@ bool ModelEngine::initializeQuantifier( Node f ){
// Notice() << "Unhandled phase req: " << n << std::endl;
// }
//}
-
+ std::vector< Node > ics;
std::vector< Node > terms;
for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
- terms.push_back( getModelBasisTerm( f[0][j].getType() ) );
+ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
+ Node t = d_quantEngine->getTermDatabase()->getModelBasisTerm( ic.getType() );
+ ics.push_back( ic );
+ terms.push_back( t );
+ //calculate the basis match for f
+ d_builder.d_quant_basis_match[f].d_map[ ic ] = t;
}
++(d_statistics.d_num_quants_init);
+ //register model basis body
+ Node n = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
+ Node gn = n.substitute( ics.begin(), ics.end(), terms.begin(), terms.end() );
+ d_quantEngine->getTermDatabase()->registerModelBasis( n, gn );
+ //add model basis instantiation
if( d_quantEngine->addInstantiation( f, terms ) ){
- return false;
+ return 1;
}else{
- //usually shouldn't happen
+ //shouldn't happen usually, but will occur if x != y is a required literal for f.
//Notice() << "No model basis for " << f << std::endl;
++(d_statistics.d_num_quants_init_fail);
}
}
- return true;
-}
-
-void ModelEngine::buildRepresentatives(){
- d_ra.clear();
- //collect all representatives for all types and store as representative alphabet
- for( int i=0; i<d_ss->getNumCardinalityTypes(); i++ ){
- TypeNode tn = d_ss->getCardinalityType( i );
- std::vector< Node > reps;
- d_ss->getRepresentatives( tn, reps );
- Assert( !reps.empty() );
- //if( (int)reps.size()!=d_ss->getCardinality( tn ) ){
- // Notice() << "InstStrategyFinteModelFind::processResetInstantiationRound: Bad representatives for type." << std::endl;
- // Notice() << " " << tn << " has cardinality " << d_ss->getCardinality( tn );
- // Notice() << " but only " << (int)reps.size() << " were given." << std::endl;
- // Unimplemented( 27 );
- //}
- Debug("fmf-model-debug") << " " << tn << " -> " << reps.size() << std::endl;
- Debug("fmf-model-debug") << " ";
- for( int i=0; i<(int)reps.size(); i++ ){
- Debug("fmf-model-debug") << reps[i] << " ";
- }
- Debug("fmf-model-debug") << std::endl;
- //set them in the alphabet
- d_ra.set( tn, reps );
-#ifdef ME_PRINT_PROCESS_TIMES
- Notice() << tn << " has " << reps.size() << " representatives. " << std::endl;
-#endif
- }
+ return 0;
}
-void ModelEngine::initializeModel(){
- d_uf_model.clear();
- d_quant_sat.clear();
- for( int k=0; k<2; k++ ){
- d_pro_con_quant[k].clear();
- }
-
- ////now analyze quantifiers (temporary)
- //for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){
- // Node f = d_quantEngine->getAssertedQuantifier( i );
- // Debug("fmf-model-req") << "Phase requirements for " << f << ": " << std::endl;
- // for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
- // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
- // Node n = it->first;
- // Debug("fmf-model-req") << " " << n << " -> " << it->second << std::endl;
- // if( n.getKind()==APPLY_UF ){
- // processPredicate( f, n, it->second );
- // }else if( n.getKind()==EQUAL ){
- // processEquality( f, n, it->second );
- // }
- // }
- //}
- for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){
- Node f = d_quantEngine->getAssertedQuantifier( i );
- initializeUf( f[1] );
- //register model basis terms
- std::vector< Node > vars;
- std::vector< Node > subs;
- for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
- vars.push_back( d_quantEngine->getInstantiationConstant( f, j ) );
- subs.push_back( getModelBasisTerm( f[0][j].getType() ) );
- }
- Node n = d_quantEngine->getCounterexampleBody( f );
- Node gn = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- registerModelBasis( n, gn );
- }
-}
-
-void ModelEngine::analyzeQuantifiers(){
- int quantSatInit = 0;
- int nquantSatInit = 0;
- //analyze the preferences of each quantifier
- for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){
- Node f = d_quantEngine->getAssertedQuantifier( i );
- Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
- std::vector< Node > pro_con[2];
- std::vector< Node > pro_con_patterns[2];
- //check which model basis terms have good and bad definitions according to f
- for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
- it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
- Node n = it->first;
- Node gn = d_model_basis[n];
- Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl;
- int pref = 0;
- bool isConst = true;
- std::vector< Node > uf_terms;
- std::vector< Node > uf_term_patterns;
- if( gn.getKind()==APPLY_UF ){
- if( d_quantEngine->getEqualityQuery()->hasTerm( gn ) ){
- uf_terms.push_back( gn );
- uf_term_patterns.push_back( n );
- bool phase = areEqual( gn, NodeManager::currentNM()->mkConst( true ) );
- pref = phase!=it->second ? 1 : -1;
- }
- }else if( gn.getKind()==EQUAL ){
- bool success = true;
- for( int j=0; j<2; j++ ){
- if( n[j].getKind()==APPLY_UF ){
- Node op = gn[j].getOperator();
- if( d_uf_model.find( op )!=d_uf_model.end() ){
- Assert( gn[j].getKind()==APPLY_UF );
- uf_terms.push_back( gn[j] );
- uf_term_patterns.push_back( n[j] );
- }else{
- //found undefined uf operator
- success = false;
- }
- }else if( n[j].hasAttribute(InstConstantAttribute()) ){
- isConst = false;
- }
- }
- if( success && !uf_terms.empty() ){
- if( (!it->second && areEqual( gn[0], gn[1] )) || (it->second && areDisequal( gn[0], gn[1] )) ){
- pref = 1;
- }else if( (it->second && areEqual( gn[0], gn[1] )) || (!it->second && areDisequal( gn[0], gn[1] )) ){
- pref = -1;
- }
- }
- }
- if( pref!=0 ){
- Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" );
- Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
- if( pref==1 ){
- if( isConst ){
- for( int j=0; j<(int)uf_terms.size(); j++ ){
- //the only uf that is initialized are those that are constant
- Node op = uf_terms[j].getOperator();
- Assert( d_uf_model.find( op )!=d_uf_model.end() );
- if( !d_uf_model[op].isConstant() ){
- isConst = false;
- break;
- }
- }
- if( isConst ){
- d_quant_sat[f] = true;
- //we only need to consider current term definition(s) for this quantifier to be satisified, ignore the others
- for( int k=0; k<2; k++ ){
- pro_con[k].clear();
- pro_con_patterns[k].clear();
- }
- //instead, just note to the model for each uf term that f is pro its definition
- for( int j=0; j<(int)uf_terms.size(); j++ ){
- Node op = uf_terms[j].getOperator();
- d_uf_model[op].d_reconsider_model = false;
- }
- }
- }
- }
- if( d_quant_sat.find( f )!=d_quant_sat.end() ){
- Debug("fmf-model-prefs") << " * Constant SAT due to definition of " << n << std::endl;
- break;
- }else{
- int pcIndex = pref==1 ? 0 : 1;
- for( int j=0; j<(int)uf_terms.size(); j++ ){
- pro_con[pcIndex].push_back( uf_terms[j] );
- pro_con_patterns[pcIndex].push_back( uf_term_patterns[j] );
- }
- }
- }
- }
- if( d_quant_sat.find( f )!=d_quant_sat.end() ){
- quantSatInit++;
- d_statistics.d_pre_sat_quant += quantSatInit;
- }else{
- nquantSatInit++;
- d_statistics.d_pre_nsat_quant += quantSatInit;
- }
- //add quantifier's preferences to vector
- for( int k=0; k<2; k++ ){
- for( int j=0; j<(int)pro_con[k].size(); j++ ){
- Node op = pro_con[k][j].getOperator();
- d_uf_model[op].setValuePreference( f, pro_con[k][j], k==0 );
- d_pro_con_quant[k][ f ].push_back( pro_con_patterns[k][j] );
- }
- }
- }
- Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
-}
-
-int ModelEngine::instantiateQuantifier( Node f ){
+int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
+ int tests = 0;
int addedLemmas = 0;
+ int triedLemmas = 0;
Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl;
Debug("inst-fmf-ei") << " Instantiation Constants: ";
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Debug("inst-fmf-ei") << d_quantEngine->getInstantiationConstant( f, i ) << " ";
+ Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
}
Debug("inst-fmf-ei") << std::endl;
- for( int k=0; k<2; k++ ){
- Debug("inst-fmf-ei") << " " << ( k==0 ? "Pro" : "Con" ) << " definitions:" << std::endl;
- for( int i=0; i<(int)d_pro_con_quant[k][f].size(); i++ ){
- Debug("inst-fmf-ei") << " " << d_pro_con_quant[k][f][i] << std::endl;
- }
- }
- if( d_pro_con_quant[0][f].empty() ){
- Debug("inst-fmf-ei") << "WARNING: " << f << " has no pros for default literal definitions" << std::endl;
- }
- d_eval_failed_lits.clear();
- d_eval_failed.clear();
- d_eval_term_model.clear();
- //d_eval_term_vals.clear();
- //d_eval_term_fv_deps.clear();
- RepAlphabetIterator riter( d_quantEngine, f, this );
- increment( &riter );
-#ifdef ONE_INST_PER_QUANT_PER_ROUND
- while( !riter.isFinished() && addedLemmas==0 ){
-#else
- while( !riter.isFinished() ){
+ if( d_builder.d_quant_selection_lits[f].empty() ){
+ Debug("inst-fmf-ei") << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl;
+#ifdef ME_PRINT_WARNINGS
+ Message() << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl;
#endif
- InstMatch m;
- riter.getMatch( d_quantEngine, m );
- Debug("fmf-model-eval") << "* Add instantiation " << std::endl;
- riter.d_inst_tried++;
- if( d_quantEngine->addInstantiation( f, m ) ){
- addedLemmas++;
- }
- riter.increment( d_quantEngine );
- increment( &riter );
- }
- if( Debug.isOn("inst-fmf-ei") ){
- int totalInst = 1;
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- totalInst = totalInst * (int)getReps()->d_type_reps[ f[0][i].getType() ].size();
- }
- Debug("inst-fmf-ei") << "Finished: " << std::endl;
- Debug("inst-fmf-ei") << " Inst Skipped: " << (totalInst-riter.d_inst_tried) << std::endl;
- Debug("inst-fmf-ei") << " Inst Tried: " << riter.d_inst_tried << std::endl;
- Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
- Debug("inst-fmf-ei") << " # Tests: " << riter.d_inst_tests << std::endl;
- }
- return addedLemmas;
-}
-
-void ModelEngine::registerModelBasis( Node n, Node gn ){
- if( d_model_basis.find( n )==d_model_basis.end() ){
- d_model_basis[n] = gn;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- registerModelBasis( n[i], gn[i] );
- }
- }
-}
-
-Node ModelEngine::getArbitraryElement( TypeNode tn, std::vector< Node >& exclude ){
- Node retVal;
- if( tn==NodeManager::currentNM()->booleanType() ){
- if( exclude.empty() ){
- retVal = NodeManager::currentNM()->mkConst( false );
- }else if( exclude.size()==1 ){
- retVal = NodeManager::currentNM()->mkConst( areEqual( exclude[0], NodeManager::currentNM()->mkConst( false ) ) );
- }
- }else if( d_ra.d_type_reps.find( tn )!=d_ra.d_type_reps.end() ){
- for( int i=0; i<(int)d_ra.d_type_reps[tn].size(); i++ ){
- if( std::find( exclude.begin(), exclude.end(), d_ra.d_type_reps[tn][i] )==exclude.end() ){
- retVal = d_ra.d_type_reps[tn][i];
- break;
- }
- }
- }
- if( !retVal.isNull() ){
- return d_quantEngine->getEqualityQuery()->getRepresentative( retVal );
}else{
- return Node::null();
- }
-}
-
-Node ModelEngine::getModelBasisTerm( TypeNode tn, int i ){
- return d_ss->getCardinalityTerm( tn );
-}
-
-Node ModelEngine::getModelBasisApplyUfTerm( Node op ){
- if( d_model_basis_term.find( op )==d_model_basis_term.end() ){
- TypeNode t = op.getType();
- std::vector< Node > children;
- children.push_back( op );
- for( int i=0; i<(int)t.getNumChildren()-1; i++ ){
- children.push_back( getModelBasisTerm( t[i] ) );
- }
- d_model_basis_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- }
- return d_model_basis_term[op];
-}
-
-bool ModelEngine::isModelBasisTerm( Node op, Node n ){
- if( n.getOperator()==op ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( !n[i].getAttribute(ModelBasisAttribute()) ){
- return false;
- }
- }
- return true;
- }else{
- return false;
- }
-}
-
-void ModelEngine::initializeUf( Node n ){
- std::vector< Node > terms;
- collectUfTerms( n, terms );
- for( int i=0; i<(int)terms.size(); i++ ){
- initializeUfModel( terms[i].getOperator() );
- }
-}
-
-void ModelEngine::collectUfTerms( Node n, std::vector< Node >& terms ){
- if( n.getKind()==APPLY_UF ){
- terms.push_back( n );
- }
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- collectUfTerms( n[i], terms );
- }
-}
-
-void ModelEngine::initializeUfModel( Node op ){
- if( d_uf_model.find( op )==d_uf_model.end() ){
- TypeNode tn = op.getType();
- tn = tn[ (int)tn.getNumChildren()-1 ];
- if( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ){
- d_uf_model[ op ] = UfModel( op, this );
- }
- }
-}
-
-void ModelEngine::makeEvalTermModel( Node n ){
- if( d_eval_term_model.find( n )==d_eval_term_model.end() ){
- makeEvalTermIndexOrder( n );
- if( !d_eval_term_use_default_model[n] ){
- Node op = n.getOperator();
- d_eval_term_model[n] = UfModelTreeOrdered( op, d_eval_term_index_order[n] );
- d_uf_model[op].makeModel( d_quantEngine, d_eval_term_model[n] );
- Debug("fmf-model-index-order") << "Make model for " << n << " : " << std::endl;
- d_eval_term_model[n].debugPrint( "fmf-model-index-order", d_quantEngine, 2 );
- }
- }
-}
-
-struct sortGetMaxVariableNum {
- std::map< Node, int > d_max_var_num;
- int computeMaxVariableNum( Node n ){
- if( n.getKind()==INST_CONSTANT ){
- return n.getAttribute(InstVarNumAttribute());
- }else if( n.hasAttribute(InstConstantAttribute()) ){
- int maxVal = -1;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- int val = getMaxVariableNum( n[i] );
- if( val>maxVal ){
- maxVal = val;
- }
- }
- return maxVal;
- }else{
- return -1;
- }
- }
- int getMaxVariableNum( Node n ){
- std::map< Node, int >::iterator it = d_max_var_num.find( n );
- if( it==d_max_var_num.end() ){
- int num = computeMaxVariableNum( n );
- d_max_var_num[n] = num;
- return num;
- }else{
- return it->second;
- }
- }
- bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
-};
-
-void ModelEngine::makeEvalTermIndexOrder( Node n ){
- if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
- //sort arguments in order of least significant vs. most significant variable in default ordering
- std::map< Node, std::vector< int > > argIndex;
- std::vector< Node > args;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( argIndex.find( n[i] )==argIndex.end() ){
- args.push_back( n[i] );
- }
- argIndex[n[i]].push_back( i );
- }
- sortGetMaxVariableNum sgmvn;
- std::sort( args.begin(), args.end(), sgmvn );
- for( int i=0; i<(int)args.size(); i++ ){
- for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
- d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
- }
- }
- bool useDefault = true;
- for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
- if( i!=d_eval_term_index_order[n][i] ){
- useDefault = false;
- break;
- }
- }
- d_eval_term_use_default_model[n] = useDefault;
- Debug("fmf-model-index-order") << "Will consider the following index ordering for " << n << " : ";
- for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
- Debug("fmf-model-index-order") << d_eval_term_index_order[n][i] << " ";
- }
- Debug("fmf-model-index-order") << std::endl;
- }
-}
-
-//void ModelEngine::processPredicate( Node f, Node p, bool phase ){
-// Node op = p.getOperator();
-// initializeUfModel( op );
-// d_uf_model[ op ].addRequirement( f, p, phase );
-//}
-//
-//void ModelEngine::processEquality( Node f, Node eq, bool phase ){
-// for( int i=0; i<2; i++ ){
-// int j = i==0 ? 1 : 0;
-// if( eq[i].getKind()==APPLY_UF && eq[i].hasAttribute(InstConstantAttribute()) ){
-// Node op = eq[i].getOperator();
-// initializeUfModel( op );
-// d_uf_model[ op ].addEqRequirement( f, eq[i], eq[j], phase );
-// }
-// }
-//}
-
-void ModelEngine::increment( RepAlphabetIterator* rai ){
- if( useModel() ){
- bool success;
- do{
- success = true;
- if( !rai->isFinished() ){
- //see if instantiation is already true in current model
- Debug("fmf-model-eval") << "Evaulating ";
- rai->debugPrintSmall("fmf-model-eval");
- //calculate represenative terms we are currently considering
- rai->calculateTerms( d_quantEngine );
- rai->d_inst_tests++;
- //if eVal is not (int)rai->d_index.size(), then the instantiation is already true in the model,
- // and eVal is the highest index in rai which we can safely iterate
- int depIndex;
- if( evaluate( rai, d_quantEngine->getCounterexampleBody( rai->d_f ), depIndex )==1 ){
- Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
- //Notice() << "Returned eVal = " << eVal << "/" << rai->d_index.size() << std::endl;
- if( depIndex<(int)rai->d_index.size() ){
-#ifdef DISABLE_EVAL_SKIP_MULTIPLE
- depIndex = (int)rai->d_index.size()-1;
-#endif
- rai->increment2( d_quantEngine, depIndex );
- success = false;
+ Debug("inst-fmf-ei") << " Model literal definitions:" << std::endl;
+ for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){
+ Debug("inst-fmf-ei") << " " << d_builder.d_quant_selection_lits[f][i] << std::endl;
+ }
+ }
+ RepSetIterator riter( f, d_quantEngine->getModel() );
+ //set the domain for the iterator (the sufficient set of instantiations to try)
+ if( useRelInstDomain ){
+ riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+ }
+ RepSetEvaluator reval( d_quantEngine->getModel(), &riter );
+ while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+ d_testLemmas++;
+ if( d_builder.optUseModel() ){
+ //see if instantiation is already true in current model
+ Debug("fmf-model-eval") << "Evaluating ";
+ riter.debugPrintSmall("fmf-model-eval");
+ Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+ tests++;
+ //if evaluate(...)==1, then the instantiation is already true in the model
+ // depIndex is the index of the least significant variable that this evaluation relies upon
+ int depIndex = riter.getNumTerms()-1;
+ int eval = reval.evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex );
+ if( eval==1 ){
+ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
+ riter.increment2( depIndex );
+ }else{
+ Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+ InstMatch m;
+ riter.getMatch( d_quantEngine, m );
+ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+ triedLemmas++;
+ d_triedLemmas++;
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ addedLemmas++;
+#ifdef EVAL_FAIL_SKIP_MULTIPLE
+ if( eval==-1 ){
+ riter.increment2( depIndex );
+ }else{
+ riter.increment();
}
+#else
+ riter.increment();
+#endif
}else{
- Debug("fmf-model-eval") << " Returned failure." << std::endl;
- }
- }
- }while( !success );
- }
-}
-
-//if evaluate( rai, n, phaseReq ) = eVal,
-// if eVal = rai->d_index.size()
-// then the formula n instantiated with rai cannot be proven to be equal to phaseReq
-// otherwise,
-// each n{rai->d_index[0]/x_0...rai->d_index[eVal]/x_eVal, */x_(eVal+1) ... */x_n } is equal to phaseReq in the current model
-int ModelEngine::evaluate( RepAlphabetIterator* rai, Node n, int& depIndex ){
- ++(d_statistics.d_eval_formulas);
- //Debug("fmf-model-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
- if( n.getKind()==NOT ){
- int val = evaluate( rai, n[0], depIndex );
- return val==1 ? -1 : ( val==-1 ? 1 : 0 );
- }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
- int baseVal = n.getKind()==AND ? 1 : -1;
- int eVal = baseVal;
- int posDepIndex = (int)rai->d_index.size();
- int negDepIndex = -1;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- //evaluate subterm
- int childDepIndex;
- Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
- int eValT = evaluate( rai, nn, childDepIndex );
- if( eValT==baseVal ){
- if( eVal==baseVal ){
- if( childDepIndex>negDepIndex ){
- negDepIndex = childDepIndex;
- }
- }
- }else if( eValT==-baseVal ){
- eVal = -baseVal;
- if( childDepIndex<posDepIndex ){
- posDepIndex = childDepIndex;
- if( posDepIndex==-1 ){
- break;
- }
- }
- }else if( eValT==0 ){
- if( eVal==baseVal ){
- eVal = 0;
+ Debug("ajr-temp") << "* Failed Add instantiation " << m << std::endl;
+ riter.increment();
}
}
- }
- if( eVal!=0 ){
- depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
- return eVal;
- }else{
- return 0;
- }
- }else if( n.getKind()==IFF || n.getKind()==XOR ){
- int depIndex1;
- int eVal = evaluate( rai, n[0], depIndex1 );
- if( eVal!=0 ){
- int depIndex2;
- int eVal2 = evaluate( rai, n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 );
- if( eVal2!=0 ){
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eVal==eVal2 ? 1 : -1;
- }
- }
- return 0;
- }else if( n.getKind()==ITE ){
- int depIndex1;
- int eVal = evaluate( rai, n[0], depIndex1 );
- if( eVal==0 ){
- //DO_THIS: evaluate children to see if they are the same value?
- return 0;
}else{
- int depIndex2;
- int eValT = evaluate( rai, n[eVal==1 ? 1 : 2], depIndex2 );
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eValT;
- }
- }else if( n.getKind()==FORALL ){
- return 0;
- }else{
- ////if we know we will fail again, immediately return
- //if( d_eval_failed.find( n )!=d_eval_failed.end() ){
- // if( d_eval_failed[n] ){
- // return -1;
- // }
- //}
- //Debug("fmf-model-eval-debug") << "Evaluate literal " << n << std::endl;
- //this should be a literal
- Node gn = n.substitute( rai->d_ic.begin(), rai->d_ic.end(), rai->d_terms.begin(), rai->d_terms.end() );
- //Debug("fmf-model-eval-debug") << " Ground version = " << gn << std::endl;
- int retVal = 0;
- std::vector< Node > fv_deps;
- if( n.getKind()==APPLY_UF ){
- //case for boolean predicates
- Node val = evaluateTerm( n, gn, fv_deps );
- if( d_quantEngine->getEqualityQuery()->hasTerm( val ) ){
- if( areEqual( val, NodeManager::currentNM()->mkConst( true ) ) ){
- retVal = 1;
- }else{
- retVal = -1;
- }
- }
- }else if( n.getKind()==EQUAL ){
- //case for equality
- retVal = evaluateEquality( n[0], n[1], gn[0], gn[1], fv_deps );
- }
- if( retVal!=0 ){
- int maxIndex = -1;
- for( int i=0; i<(int)fv_deps.size(); i++ ){
- int index = rai->d_var_order[ fv_deps[i].getAttribute(InstVarNumAttribute()) ];
- if( index>maxIndex ){
- maxIndex = index;
- if( index==(int)rai->d_index.size()-1 ){
- break;
- }
- }
+ InstMatch m;
+ riter.getMatch( d_quantEngine, m );
+ Debug("fmf-model-eval") << "* Add instantiation " << std::endl;
+ triedLemmas++;
+ d_triedLemmas++;
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ addedLemmas++;
}
- Debug("fmf-model-eval-debug") << "Evaluate literal: return " << retVal << ", depends = " << maxIndex << std::endl;
- depIndex = maxIndex;
+ riter.increment();
}
- return retVal;
- }
-}
-
-int ModelEngine::evaluateEquality( Node n1, Node n2, Node gn1, Node gn2, std::vector< Node >& fv_deps ){
- ++(d_statistics.d_eval_eqs);
- Debug("fmf-model-eval-debug") << "Evaluate equality: " << std::endl;
- Debug("fmf-model-eval-debug") << " " << n1 << " = " << n2 << std::endl;
- Debug("fmf-model-eval-debug") << " " << gn1 << " = " << gn2 << std::endl;
- Node val1 = evaluateTerm( n1, gn1, fv_deps );
- Node val2 = evaluateTerm( n2, gn2, fv_deps );
- Debug("fmf-model-eval-debug") << " Values : ";
- printRepresentative( "fmf-model-eval-debug", d_quantEngine, val1 );
- Debug("fmf-model-eval-debug") << " = ";
- printRepresentative( "fmf-model-eval-debug", d_quantEngine, val2 );
- Debug("fmf-model-eval-debug") << std::endl;
- int retVal = 0;
- if( areEqual( val1, val2 ) ){
- retVal = 1;
- }else if( areDisequal( val1, val2 ) ){
- retVal = -1;
- }
- if( retVal!=0 ){
- Debug("fmf-model-eval-debug") << " ---> Success, value = " << (retVal==1) << std::endl;
- }else{
- Debug("fmf-model-eval-debug") << " ---> Failed" << std::endl;
- }
- Debug("fmf-model-eval-debug") << " Value depends on variables: ";
- for( int i=0; i<(int)fv_deps.size(); i++ ){
- Debug("fmf-model-eval-debug") << fv_deps[i] << " ";
}
- Debug("fmf-model-eval-debug") << std::endl;
- return retVal;
-}
-
-Node ModelEngine::evaluateTerm( Node n, Node gn, std::vector< Node >& fv_deps ){
- if( n.hasAttribute(InstConstantAttribute()) ){
- if( n.getKind()==INST_CONSTANT ){
- fv_deps.push_back( n );
- return gn;
- //}else if( d_eval_term_fv_deps.find( n )!=d_eval_term_fv_deps.end() &&
- // d_eval_term_fv_deps[n].find( gn )!=d_eval_term_fv_deps[n].end() ){
- // fv_deps.insert( fv_deps.end(), d_eval_term_fv_deps[n][gn].begin(), d_eval_term_fv_deps[n][gn].end() );
- // return d_eval_term_vals[gn];
- }else{
- //Debug("fmf-model-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
- //first we must evaluate the arguments
- Node val = gn;
- if( n.getKind()==APPLY_UF ){
- Node op = gn.getOperator();
- //if it is a defined UF, then consult the interpretation
- Node gnn = gn;
- ++(d_statistics.d_eval_uf_terms);
- int depIndex = 0;
- //first we must evaluate the arguments
- bool childrenChanged = false;
- std::vector< Node > children;
- children.push_back( op );
- std::map< int, std::vector< Node > > children_var_deps;
- //for each argument, calculate its value, and the variables its value depends upon
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- Node nn = evaluateTerm( n[i], gn[i], children_var_deps[i] );
- children.push_back( nn );
- childrenChanged = childrenChanged || nn!=gn[i];
- }
- //remake gn if changed
- if( childrenChanged ){
- gnn = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- }
- if( d_uf_model.find( op )!=d_uf_model.end() ){
-#ifdef USE_INDEX_ORDERING
- //make the term model specifically for n
- makeEvalTermModel( n );
- //now, consult the model
- if( d_eval_term_use_default_model[n] ){
- val = d_uf_model[op].d_tree.getValue( d_quantEngine, gnn, depIndex );
- }else{
- val = d_eval_term_model[ n ].getValue( d_quantEngine, gnn, depIndex );
- }
- //Debug("fmf-model-eval-debug") << "Evaluate term " << n << " (" << gn << ", " << gnn << ")" << std::endl;
- //d_eval_term_model[ n ].debugPrint("fmf-model-eval-debug", d_quantEngine );
- Assert( !val.isNull() );
-#else
- //now, consult the model
- val = d_uf_model[op].d_tree.getValue( d_quantEngine, gnn, depIndex );
-#endif
- }else{
- d_eval_term_use_default_model[n] = true;
- val = gnn;
- depIndex = (int)n.getNumChildren();
- }
- Debug("fmf-model-eval-debug") << "Evaluate term " << n << " = " << gn << " = " << gnn << " = ";
- printRepresentative( "fmf-model-eval-debug", d_quantEngine, val );
- Debug("fmf-model-eval-debug") << ", depIndex = " << depIndex << std::endl;
- if( !val.isNull() ){
-#ifdef USE_INDEX_ORDERING
- for( int i=0; i<depIndex; i++ ){
- int index = d_eval_term_use_default_model[n] ? i : d_eval_term_index_order[n][i];
- Debug("fmf-model-eval-debug") << "Add variables from " << index << "..." << std::endl;
- fv_deps.insert( fv_deps.end(), children_var_deps[index].begin(),
- children_var_deps[index].end() );
- }
-#else
- //calculate the free variables that the value depends on : take those in children_var_deps[0...depIndex-1]
- for( std::map< int, std::vector< Node > >::iterator it = children_var_deps.begin(); it != children_var_deps.end(); ++it ){
- if( it->first<depIndex ){
- fv_deps.insert( fv_deps.end(), it->second.begin(), it->second.end() );
- }
- }
-#endif
- }
- ////cache the result
- //d_eval_term_vals[gn] = val;
- //d_eval_term_fv_deps[n][gn].insert( d_eval_term_fv_deps[n][gn].end(), fv_deps.begin(), fv_deps.end() );
+ d_statistics.d_eval_formulas += reval.d_eval_formulas;
+ d_statistics.d_eval_eqs += reval.d_eval_eqs;
+ d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms;
+ int totalInst = 1;
+ int relevantInst = 1;
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ totalInst = totalInst * (int)d_quantEngine->getModel()->d_ra.d_type_reps[ f[0][i].getType() ].size();
+ relevantInst = relevantInst * (int)riter.d_domain[i].size();
+ }
+ d_totalLemmas += totalInst;
+ d_relevantLemmas += relevantInst;
+ Debug("inst-fmf-ei") << "Finished: " << std::endl;
+ Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
+ Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
+ Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
+ Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
+ Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl;
+///-----------
+#ifdef ME_PRINT_WARNINGS
+ if( addedLemmas>1000 ){
+ Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+ Notice() << " Inst Total: " << totalInst << std::endl;
+ Notice() << " Inst Relevant: " << totalRelevant << std::endl;
+ Notice() << " Inst Tried: " << triedLemmas << std::endl;
+ Notice() << " Inst Added: " << addedLemmas << std::endl;
+ Notice() << " # Tests: " << tests << std::endl;
+ Notice() << std::endl;
+ if( !d_builder.d_quant_selection_lits[f].empty() ){
+ Notice() << " Model literal definitions:" << std::endl;
+ for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){
+ Notice() << " " << d_builder.d_quant_selection_lits[f][i] << std::endl;
}
- return val;
+ Notice() << std::endl;
}
- }else{
- return n;
- }
-}
-
-void ModelEngine::clearEvalFailed( int index ){
- for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
- d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
}
- d_eval_failed_lits[index].clear();
-}
-
-bool ModelEngine::areEqual( Node a, Node b ){
- return d_quantEngine->getEqualityQuery()->areEqual( a, b );
-}
-
-bool ModelEngine::areDisequal( Node a, Node b ){
- return d_quantEngine->getEqualityQuery()->areDisequal( a, b );
+#endif
+///-----------
+ return addedLemmas;
}
void ModelEngine::debugPrint( const char* c ){
- Debug( c ) << "---Current Model---" << std::endl;
- Debug( c ) << "Representatives: " << std::endl;
- d_ra.debugPrint( c, d_quantEngine );
Debug( c ) << "Quantifiers: " << std::endl;
- for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){
- Node f = d_quantEngine->getAssertedQuantifier( i );
+ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
Debug( c ) << " ";
- if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+ if( d_builder.d_quant_sat.find( f )!=d_builder.d_quant_sat.end() ){
Debug( c ) << "*SAT* ";
}else{
Debug( c ) << " ";
}
Debug( c ) << f << std::endl;
}
- Debug( c ) << "Functions: " << std::endl;
- for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
- it->second.debugPrint( c );
- Debug( c ) << std::endl;
- }
+ //d_quantEngine->getModel()->debugPrint( c );
}
ModelEngine::Statistics::Statistics():
d_inst_rounds("ModelEngine::Inst_Rounds", 0),
- d_pre_sat_quant("ModelEngine::Status_quant_pre_sat", 0),
- d_pre_nsat_quant("ModelEngine::Status_quant_pre_non_sat", 0),
d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
d_eval_eqs("ModelEngine::Eval_Equalities", 0 ),
d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
@@ -1380,8 +663,6 @@ ModelEngine::Statistics::Statistics():
d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 )
{
StatisticsRegistry::registerStat(&d_inst_rounds);
- StatisticsRegistry::registerStat(&d_pre_sat_quant);
- StatisticsRegistry::registerStat(&d_pre_nsat_quant);
StatisticsRegistry::registerStat(&d_eval_formulas);
StatisticsRegistry::registerStat(&d_eval_eqs);
StatisticsRegistry::registerStat(&d_eval_uf_terms);
@@ -1391,11 +672,11 @@ ModelEngine::Statistics::Statistics():
ModelEngine::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_inst_rounds);
- StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
- StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
StatisticsRegistry::unregisterStat(&d_eval_formulas);
StatisticsRegistry::unregisterStat(&d_eval_eqs);
StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
StatisticsRegistry::unregisterStat(&d_num_quants_init);
StatisticsRegistry::unregisterStat(&d_num_quants_init_fail);
}
+
+
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index cf6691918..b01139826 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -11,7 +11,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Instantiation Engine classes
+ ** \brief Model Engine classes
**/
#include "cvc4_private.h"
@@ -21,6 +21,9 @@
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/model.h"
+#include "theory/uf/theory_uf_model.h"
+#include "theory/quantifiers/relevant_domain.h"
namespace CVC4 {
namespace theory {
@@ -31,312 +34,87 @@ namespace uf{
namespace quantifiers {
-/** this class stores a representative alphabet */
-class RepAlphabet {
-public:
- RepAlphabet(){}
- RepAlphabet( RepAlphabet& ra, QuantifiersEngine* qe );
- ~RepAlphabet(){}
- std::map< TypeNode, std::vector< Node > > d_type_reps;
- std::map< Node, int > d_tmap;
- /** clear the alphabet */
- void clear(){
- d_type_reps.clear();
- d_tmap.clear();
- }
- /** set the representatives for type */
- void set( TypeNode t, std::vector< Node >& reps );
- /** returns index in d_type_reps for node n */
- int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; }
- /** debug print */
- void debugPrint( const char* c, QuantifiersEngine* qe );
-};
-
-class ModelEngine;
-
-/** this class iterates over a RepAlphabet */
-class RepAlphabetIterator {
-private:
- void initialize( QuantifiersEngine* qe, Node f, ModelEngine* model );
-public:
- RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model );
- RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model, std::vector< int >& indexOrder );
- ~RepAlphabetIterator(){}
- //pointer to quantifier
- Node d_f;
- //pointer to model
- ModelEngine* d_model;
- //index we are considering
- std::vector< int > d_index;
- //ordering for variables we are indexing over
- // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
- // then we consider instantiations in this order:
- // a/x a/y a/z
- // a/x b/y a/z
- // b/x a/y a/z
- // b/x b/y a/z
- // ...
- std::vector< int > d_index_order;
- //variables to index they are considered at
- // for example, if d_index_order = { 2, 0, 1 }
- // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
- std::map< int, int > d_var_order;
- //the instantiation constants of d_f
- std::vector< Node > d_ic;
- //the current terms we are considering
- std::vector< Node > d_terms;
-public:
- /** increment the iterator */
- void increment2( QuantifiersEngine* qe, int counter );
- void increment( QuantifiersEngine* qe );
- /** is the iterator finished? */
- bool isFinished();
- /** produce the match that this iterator represents */
- void getMatch( QuantifiersEngine* qe, InstMatch& m );
- /** get the i_th term we are considering */
- Node getTerm( int i );
- /** get the number of terms we are considering */
- int getNumTerms() { return d_f[0].getNumChildren(); }
- /** refresh d_term to be current with d_index */
- void calculateTerms( QuantifiersEngine* qe );
- /** debug print */
- void debugPrint( const char* c );
- void debugPrintSmall( const char* c );
- //for debugging
- int d_inst_tried;
- int d_inst_tests;
-};
-
-
-class UfModelTree
-{
-public:
- UfModelTree(){}
- /** the data */
- std::map< Node, UfModelTree > d_data;
- /** the value of this tree node (if all paths lead to same value) */
- Node d_value;
-public:
- //is this model tree empty?
- bool isEmpty() { return d_data.empty(); }
- //clear
- void clear(){
- d_data.clear();
- d_value = Node::null();
- }
- /** setValue function
- *
- * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false
- *
- */
- void setValue( QuantifiersEngine* qe, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
- /** getValue function
- *
- * returns $val, the value of ground term n
- * Say n is f( t_0...t_n )
- * depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to $val
- * for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,
- * then g( a, a, a ) would return b with depIndex = 1
- * If ground = true, we are asking whether the term n is constant (assumes that all non-model basis arguments are ground)
- *
- */
- Node getValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex );
- ///** getConstant Value function
- // *
- // * given term n, where n may contain model basis arguments
- // * if n is constant for its entire domain, then this function returns the value of its domain
- // * otherwise, it returns null
- // * for example, if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,
- // * then f( a, e ) would return b, while f( e, a ) would return null
- // *
- // */
- Node getConstantValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int argIndex );
- /** simplify function */
- void simplify( Node op, Node defaultVal, int argIndex );
- // is total ?
- bool isTotal( Node op, int argIndex );
-public:
- void debugPrint( const char* c, QuantifiersEngine* qe, std::vector< int >& indexOrder, int ind = 0, int arg = 0 );
-};
-class UfModelTreeOrdered
+//the model builder
+class ModelEngineBuilder : public TheoryEngineModelBuilder
{
-private:
- Node d_op;
- std::vector< int > d_index_order;
- UfModelTree d_tree;
-public:
- UfModelTreeOrdered(){}
- UfModelTreeOrdered( Node op ) : d_op( op ){
- TypeNode tn = d_op.getType();
- for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){
- d_index_order.push_back( i );
- }
- }
- UfModelTreeOrdered( Node op, std::vector< int >& indexOrder ) : d_op( op ){
- d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() );
- }
- bool isEmpty() { return d_tree.isEmpty(); }
- void clear() { d_tree.clear(); }
- void setValue( QuantifiersEngine* qe, Node n, Node v, bool ground = true ){
- d_tree.setValue( qe, n, v, d_index_order, ground, 0 );
- }
- Node getValue( QuantifiersEngine* qe, Node n, int& depIndex ){
- return d_tree.getValue( qe, n, d_index_order, depIndex, 0 );
- }
- Node getConstantValue( QuantifiersEngine* qe, Node n ) {
- return d_tree.getConstantValue( qe, n, d_index_order, 0 );
- }
- void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }
- bool isTotal() { return d_tree.isTotal( d_op, 0 ); }
-public:
- void debugPrint( const char* c, QuantifiersEngine* qe, int ind = 0 ){
- d_tree.debugPrint( c, qe, d_index_order, ind );
- }
-};
-
-class UfModel
-{
-//public:
- //std::map< Node, std::vector< Node > > d_reqs[2];
- //std::map< Node, std::map< Node, std::vector< Node > > > d_eq_reqs[2];
- ///** add requirement */
- //void addRequirement( Node f, Node p, bool phase ) { d_reqs[ phase ? 1 : 0 ][ f ].push_back( p ); }
- ///** add equality requirement */
- //void addEqRequirement( Node f, Node t, Node te, bool phase ) { d_eq_reqs[ phase ? 1 : 0 ][ f ][ t ].push_back( te ); }
-private:
- Node d_op;
- ModelEngine* d_me;
- std::vector< Node > d_ground_asserts;
- std::vector< Node > d_ground_asserts_reps;
- bool d_model_constructed;
- //store for set values
- std::map< Node, Node > d_set_values[2];
- // preferences for default values
- std::vector< Node > d_values;
- std::map< Node, std::vector< Node > > d_value_pro_con[2];
- /** set value */
- void setValue( Node n, Node v, bool ground = true );
- /** set model */
- void setModel();
- /** clear model */
- void clearModel();
-public:
- UfModel(){}
- UfModel( Node op, ModelEngine* qe );
- ~UfModel(){}
- //data structure that stores the model
- UfModelTreeOrdered d_tree;
- //quantifiers that are satisfied because of the constant definition of d_op
- bool d_reconsider_model;
-public:
- /** debug print */
- void debugPrint( const char* c );
- /** get constant value */
- Node getConstantValue( QuantifiersEngine* qe, Node n );
- /** is empty */
- bool isEmpty() { return d_ground_asserts.empty(); }
- /** is constant */
- bool isConstant();
-public:
- /** build model */
- void buildModel();
- /** make model */
- void makeModel( QuantifiersEngine* qe, UfModelTreeOrdered& tree );
-public:
- /** set value preference */
- void setValuePreference( Node f, Node n, bool isPro );
+protected:
+ //quantifiers engine
+ QuantifiersEngine* d_qe;
+ //map from operators to model preference data
+ std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
+ /** choose representative */
+ Node chooseRepresentative( TheoryModel* tm, Node eqc );
+ /** use constants for representatives */
+ void processBuildModel( TheoryModel* m );
+ //analyze quantifiers
+ void analyzeQuantifiers( FirstOrderModel* fm );
+ //build model
+ void finishBuildModel( FirstOrderModel* fm );
+ //theory-specific build models
+ void finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model );
+ //do InstGen techniques for quantifier, return number of lemmas produced
+ int doInstGen( FirstOrderModel* fm, Node f );
+public:
+ ModelEngineBuilder( QuantifiersEngine* qe );
+ virtual ~ModelEngineBuilder(){}
+public:
+ /** number of lemmas generated while building model */
+ int d_addedLemmas;
+ //map from quantifiers to if are constant SAT
+ std::map< Node, bool > d_quant_sat;
+ //map from quantifiers to the instantiation literals that their model is dependent upon
+ std::map< Node, std::vector< Node > > d_quant_selection_lits;
+public:
+ //map from quantifiers to model basis match
+ std::map< Node, InstMatch > d_quant_basis_match;
+ //options
+ bool optUseModel();
+ bool optInstGen();
+ bool optOneQuantPerRoundInstGen();
+ /** statistics class */
+ class Statistics {
+ public:
+ IntStat d_pre_sat_quant;
+ IntStat d_pre_nsat_quant;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
};
-
-
-
class ModelEngine : public QuantifiersModule
{
- friend class UfModel;
- friend class RepAlphabetIterator;
+ friend class uf::UfModel;
+ friend class RepSetIterator;
private:
- TheoryQuantifiers* d_th;
- QuantifiersEngine* d_quantEngine;
- uf::StrongSolverTheoryUf* d_ss;
+ /** builder class */
+ ModelEngineBuilder d_builder;
+private: //data maintained globally:
//which quantifiers have been initialized
std::map< Node, bool > d_quant_init;
- //map from ops to model basis terms
- std::map< Node, Node > d_model_basis_term;
- //map from instantiation terms to their model basis equivalent
- std::map< Node, Node > d_model_basis;
- //the model we are working with
- RepAlphabet d_ra;
- std::map< Node, UfModel > d_uf_model;
- ////map from model basis terms to quantifiers that are pro/con their definition
- //std::map< Node, std::vector< Node > > d_quant_pro_con[2];
- //map from quantifiers to model basis terms that are pro the definition of
- std::map< Node, std::vector< Node > > d_pro_con_quant[2];
- //map from quantifiers to if are constant SAT
- std::map< Node, bool > d_quant_sat;
+private: //analysis of current model:
+ //relevant domain
+ RelevantDomain d_rel_domain;
private:
- int evaluate( RepAlphabetIterator* rai, Node n, int& depIndex );
- int evaluateEquality( Node n1, Node n2, Node gn1, Node gn2, std::vector< Node >& fv_deps );
- Node evaluateTerm( Node n, Node gn, std::vector< Node >& fv_deps );
- //temporary storing which literals have failed
- void clearEvalFailed( int index );
- std::map< Node, bool > d_eval_failed;
- std::map< int, std::vector< Node > > d_eval_failed_lits;
- ////temporary storing for values/free variable dependencies
- //std::map< Node, Node > d_eval_term_vals;
- //std::map< Node, std::map< Node, std::vector< Node > > > d_eval_term_fv_deps;
+ //options
+ bool optOneInstPerQuantRound();
+ bool optUseRelevantDomain();
+ bool optOneQuantPerRound();
private:
- //map from terms to the models used to calculate their value
- std::map< Node, UfModelTreeOrdered > d_eval_term_model;
- std::map< Node, bool > d_eval_term_use_default_model;
- void makeEvalTermModel( Node n );
- //index ordering to use for each term
- std::map< Node, std::vector< int > > d_eval_term_index_order;
- int getMaxVariableNum( int n );
- void makeEvalTermIndexOrder( Node n );
-public:
- void increment( RepAlphabetIterator* rai );
+ //initialize quantifiers, return number of lemmas produced
+ int initializeQuantifier( Node f );
+ //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
+ int exhaustiveInstantiate( Node f, bool useRelInstDomain = false );
private:
- //queries about equality
- bool areEqual( Node a, Node b );
- bool areDisequal( Node a, Node b );
-private:
- bool useModel();
-private:
- //initialize quantifiers, return false if lemma needed to be added
- bool initializeQuantifier( Node f );
- //build representatives
- void buildRepresentatives();
- //initialize model
- void initializeModel();
- //analyze quantifiers
- void analyzeQuantifiers();
- //instantiate quantifier, return number of lemmas produced
- int instantiateQuantifier( Node f );
-private:
- //register instantiation terms with their corresponding model basis terms
- void registerModelBasis( Node n, Node gn );
- //for building UF model
- void initializeUf( Node n );
- void collectUfTerms( Node n, std::vector< Node >& terms );
- void initializeUfModel( Node op );
- //void processPredicate( Node f, Node p, bool phase );
- //void processEquality( Node f, Node eq, bool phase );
+ //temporary statistics
+ int d_triedLemmas;
+ int d_testLemmas;
+ int d_totalLemmas;
+ int d_relevantLemmas;
public:
- ModelEngine( TheoryQuantifiers* th );
+ ModelEngine( QuantifiersEngine* qe );
~ModelEngine(){}
- //get quantifiers engine
- QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
- //get representatives
- RepAlphabet* getReps() { return &d_ra; }
- //get arbitrary element
- Node getArbitraryElement( TypeNode tn, std::vector< Node >& exclude );
- //get model basis term
- Node getModelBasisTerm( TypeNode tn, int i = 0 );
- //get model basis term for op
- Node getModelBasisApplyUfTerm( Node op );
- //is model basis term for op
- bool isModelBasisTerm( Node op, Node n );
public:
void check( Theory::Effort e );
void registerQuantifier( Node f );
@@ -349,8 +127,6 @@ public:
class Statistics {
public:
IntStat d_inst_rounds;
- IntStat d_pre_sat_quant;
- IntStat d_pre_nsat_quant;
IntStat d_eval_formulas;
IntStat d_eval_eqs;
IntStat d_eval_uf_terms;
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
new file mode 100644
index 000000000..e7ae1d1c7
--- /dev/null
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -0,0 +1,173 @@
+/********************* */
+/*! \file relevant_domain.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 relevant domain class
+ **/
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){
+
+}
+
+void RelevantDomain::compute(){
+ d_quant_inst_domain.clear();
+ for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_model->getAssertedQuantifier( i );
+ d_quant_inst_domain[f].resize( f[0].getNumChildren() );
+ }
+ //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)
+ for( std::map< Node, uf::UfModel >::iterator it = d_model->d_uf_model.begin();
+ it != d_model->d_uf_model.end(); ++it ){
+ Node op = it->first;
+ for( int i=0; i<(int)it->second.d_ground_asserts.size(); i++ ){
+ Node n = it->second.d_ground_asserts[i];
+ //add arguments to domain
+ for( int j=0; j<(int)n.getNumChildren(); j++ ){
+ if( d_model->d_ra.hasType( n[j].getType() ) ){
+ Node ra = d_model->getRepresentative( n[j] );
+ int raIndex = d_model->d_ra.getIndexFor( ra );
+ Assert( raIndex!=-1 );
+ if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){
+ d_active_domain[op][j].push_back( raIndex );
+ }
+ }
+ }
+ //add to range
+ Node r = it->second.d_ground_asserts_reps[i];
+ int raIndex = d_model->d_ra.getIndexFor( r );
+ Assert( raIndex!=-1 );
+ if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){
+ d_active_range[op].push_back( raIndex );
+ }
+ }
+ }
+ //find fixed point for relevant domain computation
+ bool success;
+ do{
+ success = true;
+ for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_model->getAssertedQuantifier( i );
+ //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)
+ if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){
+ success = false;
+ }
+ //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)
+ RepDomain range;
+ if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){
+ success = false;
+ }
+ }
+ }while( !success );
+}
+
+bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){
+ bool domainChanged = false;
+ if( n.getKind()==INST_CONSTANT ){
+ bool domainSet = false;
+ int vi = n.getAttribute(InstVarNumAttribute());
+ Assert( !parent.isNull() );
+ if( parent.getKind()==APPLY_UF ){
+ //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument
+ Node op = parent.getOperator();
+ if( d_active_domain.find( op )!=d_active_domain.end() ){
+ for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){
+ int d = d_active_domain[op][arg][i];
+ if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){
+ rd[vi].push_back( d );
+ domainChanged = true;
+ }
+ }
+ domainSet = true;
+ }
+ }
+ if( !domainSet ){
+ //otherwise, we must consider the entire domain
+ TypeNode tn = n.getType();
+ if( d_model->d_ra.hasType( tn ) ){
+ if( rd[vi].size()!=d_model->d_ra.d_type_reps[tn].size() ){
+ rd[vi].clear();
+ for( size_t i=0; i<d_model->d_ra.d_type_reps[tn].size(); i++ ){
+ rd[vi].push_back( i );
+ domainChanged = true;
+ }
+ }
+ }else{
+ //infinite domain?
+ }
+ }
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){
+ domainChanged = true;
+ }
+ }
+ }
+ return domainChanged;
+}
+
+bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
+ if( n.getKind()==INST_CONSTANT ){
+ Node f = n.getAttribute(InstConstantAttribute());
+ int var = n.getAttribute(InstVarNumAttribute());
+ range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );
+ return false;
+ }else{
+ Node op;
+ if( n.getKind()==APPLY_UF ){
+ op = n.getOperator();
+ }
+ bool domainChanged = false;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ RepDomain childRange;
+ if( extendFunctionDomains( n[i], childRange ) ){
+ domainChanged = true;
+ }
+ if( n.getKind()==APPLY_UF ){
+ if( d_active_domain.find( op )!=d_active_domain.end() ){
+ for( int j=0; j<(int)childRange.size(); j++ ){
+ int v = childRange[j];
+ if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){
+ d_active_domain[op][i].push_back( v );
+ domainChanged = true;
+ }
+ }
+ }else{
+ //do this?
+ }
+ }
+ }
+ //get the range
+ if( n.hasAttribute(InstConstantAttribute()) ){
+ if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){
+ range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );
+ }else{
+ //infinite range?
+ }
+ }else{
+ Node r = d_model->getRepresentative( n );
+ range.push_back( d_model->d_ra.getIndexFor( r ) );
+ }
+ return domainChanged;
+ }
+} \ No newline at end of file
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
new file mode 100644
index 000000000..362a39d6a
--- /dev/null
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -0,0 +1,54 @@
+/********************* */
+/*! \file relevant_domain.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 relevant domain class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__RELEVANT_DOMAIN_H
+#define __CVC4__RELEVANT_DOMAIN_H
+
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class RelevantDomain
+{
+private:
+ FirstOrderModel* d_model;
+
+ //the domain of the arguments for each operator
+ std::map< Node, std::map< int, RepDomain > > d_active_domain;
+ //the range for each operator
+ std::map< Node, RepDomain > d_active_range;
+ //for computing relevant instantiation domain, return true if changed
+ bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd );
+ //for computing extended
+ bool extendFunctionDomains( Node n, RepDomain& range );
+public:
+ RelevantDomain( FirstOrderModel* m );
+ virtual ~RelevantDomain(){}
+ //compute the relevant domain
+ void compute();
+ //relevant instantiation domain for each quantifier
+ std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp
new file mode 100644
index 000000000..02041480f
--- /dev/null
+++ b/src/theory/quantifiers/rep_set_iterator.cpp
@@ -0,0 +1,523 @@
+/********************* */
+/*! \file rep_set_iterator.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 relevant domain class
+ **/
+
+#include "theory/quantifiers/rep_set_iterator.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+#define USE_INDEX_ORDERING
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){
+ //store instantiation constants
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ d_index.push_back( 0 );
+ }
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ //store default index order
+ d_index_order.push_back( i );
+ d_var_order[i] = i;
+ //store default domain
+ d_domain.push_back( RepDomain() );
+ for( int j=0; j<(int)d_model->d_ra.d_type_reps[d_f[0][i].getType()].size(); j++ ){
+ d_domain[i].push_back( j );
+ }
+ }
+}
+
+void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
+ d_index_order.clear();
+ d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
+ //make the d_var_order mapping
+ for( int i=0; i<(int)d_index_order.size(); i++ ){
+ d_var_order[d_index_order[i]] = i;
+ }
+}
+
+void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
+ d_domain.clear();
+ d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
+ //we are done if a domain is empty
+ for( int i=0; i<(int)d_domain.size(); i++ ){
+ if( d_domain[i].empty() ){
+ d_index.clear();
+ }
+ }
+}
+
+void RepSetIterator::increment2( int counter ){
+ Assert( !isFinished() );
+#ifdef DISABLE_EVAL_SKIP_MULTIPLE
+ counter = (int)d_index.size()-1;
+#endif
+ //increment d_index
+ while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){
+ counter--;
+ }
+ if( counter==-1 ){
+ d_index.clear();
+ }else{
+ for( int i=(int)d_index.size()-1; i>counter; i-- ){
+ d_index[i] = 0;
+ //d_model->clearEvalFailed( i );
+ }
+ d_index[counter]++;
+ //d_model->clearEvalFailed( counter );
+ }
+}
+
+void RepSetIterator::increment(){
+ if( !isFinished() ){
+ increment2( (int)d_index.size()-1 );
+ }
+}
+
+bool RepSetIterator::isFinished(){
+ return d_index.empty();
+}
+
+void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){
+ for( int i=0; i<(int)d_index.size(); i++ ){
+ m.d_map[ qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ) ] = getTerm( i );
+ }
+}
+
+Node RepSetIterator::getTerm( int i ){
+ TypeNode tn = d_f[0][d_index_order[i]].getType();
+ Assert( d_model->d_ra.d_type_reps.find( tn )!=d_model->d_ra.d_type_reps.end() );
+ int index = d_index_order[i];
+ return d_model->d_ra.d_type_reps[tn][d_domain[index][d_index[index]]];
+}
+
+void RepSetIterator::debugPrint( const char* c ){
+ for( int i=0; i<(int)d_index.size(); i++ ){
+ Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;
+ }
+}
+
+void RepSetIterator::debugPrintSmall( const char* c ){
+ Debug( c ) << "RI: ";
+ for( int i=0; i<(int)d_index.size(); i++ ){
+ Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
+ }
+ Debug( c ) << std::endl;
+}
+
+RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){
+
+}
+
+//if evaluate( n, phaseReq ) = eVal,
+// if eVal = d_riter->d_index.size()
+// then the formula n instantiated with d_riter cannot be proven to be equal to phaseReq
+// otherwise,
+// each n{d_riter->d_index[0]/x_0...d_riter->d_index[eVal]/x_eVal, */x_(eVal+1) ... */x_n } is equal to phaseReq in the current model
+int RepSetEvaluator::evaluate( Node n, int& depIndex ){
+ ++d_eval_formulas;
+ //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
+ //Notice() << "Eval " << n << std::endl;
+ if( n.getKind()==NOT ){
+ int val = evaluate( n[0], depIndex );
+ return val==1 ? -1 : ( val==-1 ? 1 : 0 );
+ }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
+ int baseVal = n.getKind()==AND ? 1 : -1;
+ int eVal = baseVal;
+ int posDepIndex = d_riter->getNumTerms();
+ int negDepIndex = -1;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ //evaluate subterm
+ int childDepIndex;
+ Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
+ int eValT = evaluate( nn, childDepIndex );
+ if( eValT==baseVal ){
+ if( eVal==baseVal ){
+ if( childDepIndex>negDepIndex ){
+ negDepIndex = childDepIndex;
+ }
+ }
+ }else if( eValT==-baseVal ){
+ eVal = -baseVal;
+ if( childDepIndex<posDepIndex ){
+ posDepIndex = childDepIndex;
+ if( posDepIndex==-1 ){
+ break;
+ }
+ }
+ }else if( eValT==0 ){
+ if( eVal==baseVal ){
+ eVal = 0;
+ }
+ }
+ }
+ if( eVal!=0 ){
+ depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
+ return eVal;
+ }else{
+ return 0;
+ }
+ }else if( n.getKind()==IFF || n.getKind()==XOR ){
+ int depIndex1;
+ int eVal = evaluate( n[0], depIndex1 );
+ if( eVal!=0 ){
+ int depIndex2;
+ int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 );
+ if( eVal2!=0 ){
+ depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+ return eVal==eVal2 ? 1 : -1;
+ }
+ }
+ return 0;
+ }else if( n.getKind()==ITE ){
+ int depIndex1, depIndex2;
+ int eVal = evaluate( n[0], depIndex1 );
+ if( eVal==0 ){
+ //evaluate children to see if they are the same value
+ int eval1 = evaluate( n[1], depIndex1 );
+ if( eval1!=0 ){
+ int eval2 = evaluate( n[1], depIndex2 );
+ if( eval1==eval2 ){
+ depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+ return eval1;
+ }
+ }
+ }else{
+ int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 );
+ depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+ return eValT;
+ }
+ return 0;
+ }else if( n.getKind()==FORALL ){
+ return 0;
+ }else{
+ ////if we know we will fail again, immediately return
+ //if( d_eval_failed.find( n )!=d_eval_failed.end() ){
+ // if( d_eval_failed[n] ){
+ // return -1;
+ // }
+ //}
+ //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
+ //this should be a literal
+ //Node gn = n.substitute( d_riter->d_ic.begin(), d_riter->d_ic.end(), d_riter->d_terms.begin(), d_riter->d_terms.end() );
+ //Debug("fmf-eval-debug") << " Ground version = " << gn << std::endl;
+ int retVal = 0;
+ depIndex = d_riter->getNumTerms()-1;
+ if( n.getKind()==APPLY_UF ){
+ //case for boolean predicates
+ Node val = evaluateTerm( n, depIndex );
+ if( d_model->hasTerm( val ) ){
+ if( d_model->areEqual( val, d_model->d_true ) ){
+ retVal = 1;
+ }else{
+ retVal = -1;
+ }
+ }
+ }else if( n.getKind()==EQUAL ){
+ //case for equality
+ retVal = evaluateEquality( n[0], n[1], depIndex );
+ }else{
+ std::vector< int > cdi;
+ Node val = evaluateTermDefault( n, depIndex, cdi );
+ if( !val.isNull() ){
+ val = Rewriter::rewrite( val );
+ if( val==d_model->d_true ){
+ retVal = 1;
+ }else if( val==d_model->d_false ){
+ retVal = -1;
+ }
+ }
+ }
+ if( retVal!=0 ){
+ Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depends = " << depIndex << std::endl;
+ }else{
+ Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
+ //std::cout << "Neither true nor false : " << n << std::endl;
+ }
+ return retVal;
+ }
+}
+
+int RepSetEvaluator::evaluateEquality( Node n1, Node n2, int& depIndex ){
+ ++d_eval_eqs;
+ //Notice() << "Eval eq " << n1 << " " << n2 << std::endl;
+ Debug("fmf-eval-debug") << "Evaluate equality: " << std::endl;
+ Debug("fmf-eval-debug") << " " << n1 << " = " << n2 << std::endl;
+ int depIndex1, depIndex2;
+ Node val1 = evaluateTerm( n1, depIndex1 );
+ Node val2 = evaluateTerm( n2, depIndex2 );
+ Debug("fmf-eval-debug") << " Values : ";
+ d_model->printRepresentativeDebug( "fmf-eval-debug", val1 );
+ Debug("fmf-eval-debug") << " = ";
+ d_model->printRepresentativeDebug( "fmf-eval-debug", val2 );
+ Debug("fmf-eval-debug") << std::endl;
+ int retVal = 0;
+ if( !val1.isNull() && !val2.isNull() ){
+ if( d_model->areEqual( val1, val2 ) ){
+ retVal = 1;
+ }else if( d_model->areDisequal( val1, val2 ) ){
+ retVal = -1;
+ }else{
+ Node eq = val1.eqNode( val2 );
+ eq = Rewriter::rewrite( eq );
+ if( eq==d_model->d_true ){
+ retVal = 1;
+ }else if( eq==d_model->d_false ){
+ retVal = -1;
+ }
+ }
+ }
+ if( retVal!=0 ){
+ depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+ Debug("fmf-eval-debug") << " value = " << (retVal==1) << ", depIndex = " << depIndex << std::endl;
+ }else{
+ depIndex = d_riter->getNumTerms()-1;
+ Debug("fmf-eval-amb") << "Neither equal nor disequal : " << n1 << " , " << n2 << std::endl;
+ //std::cout << "Neither equal nor disequal : " << n1 << " , " << n2 << std::endl;
+ }
+ return retVal;
+}
+
+Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
+ //Notice() << "Eval term " << n << std::endl;
+ if( n.hasAttribute(InstConstantAttribute()) ){
+ Node val;
+ depIndex = d_riter->getNumTerms()-1;
+ //check the type of n
+ if( n.getKind()==INST_CONSTANT ){
+ int v = n.getAttribute(InstVarNumAttribute());
+ depIndex = d_riter->d_var_order[ v ];
+ val = d_riter->getTerm( v );
+ }else if( n.getKind()==ITE ){
+ int depIndex1, depIndex2;
+ int eval = evaluate( n[0], depIndex1 );
+ if( eval==0 ){
+ //evaluate children to see if they are the same
+ Node val1 = evaluateTerm( n[ 1 ], depIndex1 );
+ Node val2 = evaluateTerm( n[ 1 ], depIndex1 );
+ if( val1==val2 ){
+ val = val1;
+ depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+ }else{
+ return Node::null();
+ }
+ }else{
+ val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 );
+ depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+ }
+ }else{
+#if 0
+ //for select, pre-process read over writes
+ if( n.getKind()==SELECT ){
+ Node selIndex = evaluateTerm( n[1], depIndex );
+ if( selIndex.isNull() ){
+ depIndex = d_riter->getNumTerms()-1;
+ return Node::null();
+ }
+ Node arr = n[0];
+ int eval = 1;
+ while( arr.getKind()==STORE && eval!=0 ){
+ int tempIndex;
+ eval = evaluateEquality( selIndex, arr[1], tempIndex );
+ depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+ if( eval==1 ){
+ val = evaluateTerm( arr[2], tempIndex );
+ depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+ return val;
+ }else if( eval==-1 ){
+ arr = arr[0];
+ }
+ }
+ n = NodeManager::currentNM()->mkNode( SELECT, arr, selIndex );
+ }
+#endif
+ //default term evaluate : evaluate all children, recreate the value
+ std::vector< int > children_depIndex;
+ val = evaluateTermDefault( n, depIndex, children_depIndex );
+ //case split on the type of term
+ if( n.getKind()==APPLY_UF ){
+ Node op = n.getOperator();
+ //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
+ //if it is a defined UF, then consult the interpretation
+ ++d_eval_uf_terms;
+ int argDepIndex = 0;
+ if( d_model->d_uf_model.find( op )!=d_model->d_uf_model.end() ){
+ //make the term model specifically for n
+ makeEvalUfModel( n );
+ //now, consult the model
+ if( d_eval_uf_use_default[n] ){
+ val = d_model->d_uf_model[op].d_tree.getValue( d_model, val, argDepIndex );
+ }else{
+ val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );
+ }
+ //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
+ //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
+ Assert( !val.isNull() );
+ }else{
+ d_eval_uf_use_default[n] = true;
+ argDepIndex = (int)n.getNumChildren();
+ }
+ //recalculate the depIndex
+ depIndex = -1;
+ for( int i=0; i<argDepIndex; i++ ){
+ int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
+ Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
+ if( children_depIndex[index]>depIndex ){
+ depIndex = children_depIndex[index];
+ }
+ }
+ Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";
+ d_model->printRepresentativeDebug( "fmf-eval-debug", val );
+ Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
+ }else if( n.getKind()==SELECT ){
+ if( d_model->d_array_model.find( n[0] )!=d_model->d_array_model.end() ){
+ //consult the default value for the array DO_THIS
+ //val = Rewriter::rewrite( val );
+ //val = d_model->d_array_model[ n[0] ];
+ val = Rewriter::rewrite( val );
+ }else{
+ val = Rewriter::rewrite( val );
+ }
+ }else{
+ val = Rewriter::rewrite( val );
+ }
+ }
+ return val;
+ }else{
+ depIndex = -1;
+ return n;
+ }
+}
+
+Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){
+ //first we must evaluate the arguments
+ std::vector< Node > children;
+ if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ depIndex = -1;
+ //for each argument, calculate its value, and the variables its value depends upon
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ childDepIndex.push_back( -1 );
+ Node nn = evaluateTerm( n[i], childDepIndex[i] );
+ if( nn.isNull() ){
+ depIndex = d_riter->getNumTerms()-1;
+ return nn;
+ }else{
+ children.push_back( nn );
+ if( childDepIndex[i]>depIndex ){
+ depIndex = childDepIndex[i];
+ }
+ }
+ }
+ //recreate the value
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+}
+
+void RepSetEvaluator::clearEvalFailed( int index ){
+ for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
+ d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
+ }
+ d_eval_failed_lits[index].clear();
+}
+
+void RepSetEvaluator::makeEvalUfModel( Node n ){
+ if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){
+ makeEvalUfIndexOrder( n );
+ if( !d_eval_uf_use_default[n] ){
+ Node op = n.getOperator();
+ d_eval_uf_model[n] = uf::UfModelTreeOrdered( op, d_eval_term_index_order[n] );
+ d_model->d_uf_model[op].makeModel( d_eval_uf_model[n] );
+ //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
+ //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
+ }
+ }
+}
+
+struct sortGetMaxVariableNum {
+ std::map< Node, int > d_max_var_num;
+ int computeMaxVariableNum( Node n ){
+ if( n.getKind()==INST_CONSTANT ){
+ return n.getAttribute(InstVarNumAttribute());
+ }else if( n.hasAttribute(InstConstantAttribute()) ){
+ int maxVal = -1;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ int val = getMaxVariableNum( n[i] );
+ if( val>maxVal ){
+ maxVal = val;
+ }
+ }
+ return maxVal;
+ }else{
+ return -1;
+ }
+ }
+ int getMaxVariableNum( Node n ){
+ std::map< Node, int >::iterator it = d_max_var_num.find( n );
+ if( it==d_max_var_num.end() ){
+ int num = computeMaxVariableNum( n );
+ d_max_var_num[n] = num;
+ return num;
+ }else{
+ return it->second;
+ }
+ }
+ bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
+};
+
+void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){
+ if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
+#ifdef USE_INDEX_ORDERING
+ //sort arguments in order of least significant vs. most significant variable in default ordering
+ std::map< Node, std::vector< int > > argIndex;
+ std::vector< Node > args;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( argIndex.find( n[i] )==argIndex.end() ){
+ args.push_back( n[i] );
+ }
+ argIndex[n[i]].push_back( i );
+ }
+ sortGetMaxVariableNum sgmvn;
+ std::sort( args.begin(), args.end(), sgmvn );
+ for( int i=0; i<(int)args.size(); i++ ){
+ for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
+ d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
+ }
+ }
+ bool useDefault = true;
+ for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
+ if( i!=d_eval_term_index_order[n][i] ){
+ useDefault = false;
+ break;
+ }
+ }
+ d_eval_uf_use_default[n] = useDefault;
+ Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : ";
+ for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
+ Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
+ }
+ Debug("fmf-index-order") << std::endl;
+#else
+ d_eval_uf_use_default[n] = true;
+#endif
+ }
+}
+
+
diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h
new file mode 100644
index 000000000..308d09a38
--- /dev/null
+++ b/src/theory/quantifiers/rep_set_iterator.h
@@ -0,0 +1,120 @@
+/********************* */
+/*! \file rep_set_iterator.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 rep_set_iterator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__REP_SET_ITERATOR_H
+#define __CVC4__REP_SET_ITERATOR_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** this class iterates over a RepSet */
+class RepSetIterator {
+public:
+ RepSetIterator( Node f, FirstOrderModel* model );
+ ~RepSetIterator(){}
+ //pointer to quantifier
+ Node d_f;
+ //pointer to model
+ FirstOrderModel* d_model;
+ //index we are considering
+ std::vector< int > d_index;
+ //domain we are considering
+ std::vector< RepDomain > d_domain;
+ //ordering for variables we are indexing over
+ // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
+ // then we consider instantiations in this order:
+ // a/x a/y a/z
+ // a/x b/y a/z
+ // b/x a/y a/z
+ // b/x b/y a/z
+ // ...
+ std::vector< int > d_index_order;
+ //variables to index they are considered at
+ // for example, if d_index_order = { 2, 0, 1 }
+ // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
+ std::map< int, int > d_var_order;
+ //the instantiation constants of d_f
+ std::vector< Node > d_ic;
+ //the current terms we are considering
+ std::vector< Node > d_terms;
+public:
+ /** set index order */
+ void setIndexOrder( std::vector< int >& indexOrder );
+ /** set domain */
+ void setDomain( std::vector< RepDomain >& domain );
+ /** increment the iterator */
+ void increment2( int counter );
+ void increment();
+ /** is the iterator finished? */
+ bool isFinished();
+ /** produce the match that this iterator represents */
+ void getMatch( QuantifiersEngine* qe, InstMatch& m );
+ /** get the i_th term we are considering */
+ Node getTerm( int i );
+ /** get the number of terms we are considering */
+ int getNumTerms() { return d_f[0].getNumChildren(); }
+ /** debug print */
+ void debugPrint( const char* c );
+ void debugPrintSmall( const char* c );
+};
+
+class RepSetEvaluator
+{
+private:
+ FirstOrderModel* d_model;
+ RepSetIterator* d_riter;
+private: //for Theory UF:
+ //map from terms to the models used to calculate their value
+ std::map< Node, bool > d_eval_uf_use_default;
+ std::map< Node, uf::UfModelTreeOrdered > d_eval_uf_model;
+ void makeEvalUfModel( Node n );
+ //index ordering to use for each term
+ std::map< Node, std::vector< int > > d_eval_term_index_order;
+ int getMaxVariableNum( int n );
+ void makeEvalUfIndexOrder( Node n );
+private:
+ //default evaluate term function
+ Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex );
+ //temporary storing which literals have failed
+ void clearEvalFailed( int index );
+ std::map< Node, bool > d_eval_failed;
+ std::map< int, std::vector< Node > > d_eval_failed_lits;
+public:
+ RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri );
+ virtual ~RepSetEvaluator(){}
+ /** evaluate functions */
+ int evaluate( Node n, int& depIndex );
+ int evaluateEquality( Node n1, Node n2, int& depIndex );
+ Node evaluateTerm( Node n, int& depIndex );
+public:
+ //statistics
+ int d_eval_formulas;
+ int d_eval_eqs;
+ int d_eval_uf_terms;
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
new file mode 100644
index 000000000..55ea693ef
--- /dev/null
+++ b/src/theory/quantifiers/term_database.cpp
@@ -0,0 +1,324 @@
+/********************* */
+/*! \file term_database.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 term databse class
+ **/
+
+ #include "theory/quantifiers/term_database.h"
+ #include "theory/quantifiers_engine.h"
+ #include "theory/uf/theory_uf_instantiator.h"
+ #include "theory/theory_engine.h"
+ #include "theory/quantifiers/first_order_model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
+ if( argIndex<(int)n.getNumChildren() ){
+ Node r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] );
+ std::map< Node, TermArgTrie >::iterator it = d_data.find( r );
+ if( it==d_data.end() ){
+ d_data[r].addTerm2( qe, n, argIndex+1 );
+ return true;
+ }else{
+ return it->second.addTerm2( qe, n, argIndex+1 );
+ }
+ }else{
+ //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
+ d_data[n].d_data.clear();
+ return false;
+ }
+ }
+
+ void TermDb::addTerm( Node n, std::vector< Node >& added, bool withinQuant ){
+ //don't add terms in quantifier bodies
+ if( !withinQuant || Options::current()->registerQuantBodyTerms ){
+ if( d_processed.find( n )==d_processed.end() ){
+ d_processed[n] = true;
+ //if this is an atomic trigger, consider adding it
+ if( Trigger::isAtomicTrigger( n ) ){
+ if( !n.hasAttribute(InstConstantAttribute()) ){
+ Debug("term-db") << "register trigger term " << n << std::endl;
+ //Notice() << "register trigger term " << n << std::endl;
+ Node op = n.getOperator();
+ d_op_map[op].push_back( n );
+ d_type_map[ n.getType() ].push_back( n );
+ added.push_back( n );
+
+ uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ addTerm( n[i], added, withinQuant );
+ if( Options::current()->efficientEMatching ){
+ if( d_parents[n[i]][op].empty() ){
+ //must add parent to equivalence class info
+ Node nir = d_ith->getRepresentative( n[i] );
+ uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir );
+ if( eci_nir ){
+ eci_nir->d_pfuns[ op ] = true;
+ }
+ }
+ //add to parent structure
+ if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){
+ d_parents[n[i]][op][i].push_back( n );
+ }
+ }
+ }
+ if( Options::current()->efficientEMatching ){
+ //new term, add n to candidate generators
+ for( int i=0; i<(int)d_ith->d_cand_gens[op].size(); i++ ){
+ d_ith->d_cand_gens[op][i]->addCandidate( n );
+ }
+ }
+ if( Options::current()->eagerInstQuant ){
+ if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
+ int addedLemmas = 0;
+ for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
+ addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
+ }
+ //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
+ d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() );
+ }
+ }
+ }
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ addTerm( n[i], added, withinQuant );
+ }
+ }
+ }
+ }
+
+ void TermDb::reset( Theory::Effort effort ){
+ int nonCongruentCount = 0;
+ int congruentCount = 0;
+ int alreadyCongruentCount = 0;
+ //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
+ for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
+ if( !it->second.empty() ){
+ if( it->second[0].getType()==NodeManager::currentNM()->booleanType() ){
+ d_pred_map_trie[ 0 ][ it->first ].d_data.clear();
+ d_pred_map_trie[ 1 ][ it->first ].d_data.clear();
+ }else{
+ d_func_map_trie[ it->first ].d_data.clear();
+ for( int i=0; i<(int)it->second.size(); i++ ){
+ Node n = it->second[i];
+ if( !n.getAttribute(NoMatchAttribute()) ){
+ if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
+ NoMatchAttribute nma;
+ n.setAttribute(nma,true);
+ congruentCount++;
+ }else{
+ nonCongruentCount++;
+ }
+ }else{
+ congruentCount++;
+ alreadyCongruentCount++;
+ }
+ }
+ }
+ }
+ }
+ for( int i=0; i<2; i++ ){
+ Node n = NodeManager::currentNM()->mkConst( i==1 );
+ eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ),
+ ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() );
+ while( !eqc.isFinished() ){
+ Node en = (*eqc);
+ if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
+ if( !en.getAttribute(NoMatchAttribute()) ){
+ Node op = en.getOperator();
+ if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
+ NoMatchAttribute nma;
+ en.setAttribute(nma,true);
+ congruentCount++;
+ }else{
+ nonCongruentCount++;
+ }
+ }else{
+ alreadyCongruentCount++;
+ }
+ }
+ ++eqc;
+ }
+ }
+ Debug("term-db-cong") << "TermDb: Reset" << std::endl;
+ Debug("term-db-cong") << "Congruent/Non-Congruent = ";
+ Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl;
+}
+
+void TermDb::registerModelBasis( Node n, Node gn ){
+ if( d_model_basis.find( n )==d_model_basis.end() ){
+ d_model_basis[n] = gn;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ registerModelBasis( n[i], gn[i] );
+ }
+ }
+}
+
+Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
+ if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
+ std::stringstream ss;
+ ss << Expr::setlanguage(Options::current()->outputLanguage);
+ ss << "e_" << tn;
+ d_model_basis_term[tn] = NodeManager::currentNM()->mkVar( ss.str(), tn );
+ ModelBasisAttribute mba;
+ d_model_basis_term[tn].setAttribute(mba,true);
+ }
+ return d_model_basis_term[tn];
+}
+
+Node TermDb::getModelBasisOpTerm( Node op ){
+ if( d_model_basis_op_term.find( op )==d_model_basis_op_term.end() ){
+ TypeNode t = op.getType();
+ std::vector< Node > children;
+ children.push_back( op );
+ for( size_t i=0; i<t.getNumChildren()-1; i++ ){
+ children.push_back( getModelBasisTerm( t[i] ) );
+ }
+ d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+ }
+ return d_model_basis_op_term[op];
+}
+
+void TermDb::computeModelBasisArgAttribute( Node n ){
+ if( !n.hasAttribute(ModelBasisArgAttribute()) ){
+ uint64_t val = 0;
+ //determine if it has model basis attribute
+ for( int j=0; j<(int)n.getNumChildren(); j++ ){
+ if( n[j].getAttribute(ModelBasisAttribute()) ){
+ val = 1;
+ break;
+ }
+ }
+ ModelBasisArgAttribute mbaa;
+ n.setAttribute( mbaa, val );
+ }
+}
+
+void TermDb::makeInstantiationConstantsFor( Node f ){
+ if( d_inst_constants.find( f )==d_inst_constants.end() ){
+ Debug("quantifiers-engine") << "Instantiation constants for " << f << " : " << std::endl;
+ for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+ d_vars[f].push_back( f[0][i] );
+ //make instantiation constants
+ Node ic = NodeManager::currentNM()->mkInstConstant( f[0][i].getType() );
+ d_inst_constants_map[ic] = f;
+ d_inst_constants[ f ].push_back( ic );
+ Debug("quantifiers-engine") << " " << ic << std::endl;
+ //set the var number attribute
+ InstVarNumAttribute ivna;
+ ic.setAttribute(ivna,i);
+ }
+ }
+}
+
+void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){
+ if( !n.hasAttribute(InstLevelAttribute()) ){
+ InstLevelAttribute ila;
+ n.setAttribute(ila,level);
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ setInstantiationLevelAttr( n[i], level );
+ }
+}
+
+
+void TermDb::setInstantiationConstantAttr( Node n, Node f ){
+ if( !n.hasAttribute(InstConstantAttribute()) ){
+ bool setAttr = false;
+ if( n.getKind()==INST_CONSTANT ){
+ setAttr = true;
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ setInstantiationConstantAttr( n[i], f );
+ if( n[i].hasAttribute(InstConstantAttribute()) ){
+ setAttr = true;
+ }
+ }
+ }
+ if( setAttr ){
+ InstConstantAttribute ica;
+ n.setAttribute(ica,f);
+ //also set the no-match attribute
+ NoMatchAttribute nma;
+ n.setAttribute(nma,true);
+ }
+ }
+}
+
+
+Node TermDb::getCounterexampleBody( Node f ){
+ std::map< Node, Node >::iterator it = d_counterexample_body.find( f );
+ if( it==d_counterexample_body.end() ){
+ makeInstantiationConstantsFor( f );
+ Node n = getSubstitutedNode( f[1], f );
+ d_counterexample_body[ f ] = n;
+ return n;
+ }else{
+ return it->second;
+ }
+}
+
+Node TermDb::getSkolemizedBody( Node f ){
+ Assert( f.getKind()==FORALL );
+ if( d_skolem_body.find( f )==d_skolem_body.end() ){
+ std::vector< Node > vars;
+ for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+ Node skv = NodeManager::currentNM()->mkSkolem( f[0][i].getType() );
+ d_skolem_constants[ f ].push_back( skv );
+ vars.push_back( f[0][i] );
+ }
+ d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(),
+ d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() );
+ if( f.hasAttribute(InstLevelAttribute()) ){
+ setInstantiationLevelAttr( d_skolem_body[ f ], f.getAttribute(InstLevelAttribute()) );
+ }
+ }
+ return d_skolem_body[ f ];
+}
+
+
+Node TermDb::getSubstitutedNode( Node n, Node f ){
+ return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
+}
+
+Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars,
+ const std::vector<Node> & inst_constants){
+ Node n2 = n.substitute( vars.begin(), vars.end(),
+ inst_constants.begin(),
+ inst_constants.end() );
+ setInstantiationConstantAttr( n2, f );
+ return n2;
+}
+
+Node TermDb::getFreeVariableForInstConstant( Node n ){
+ TypeNode tn = n.getType();
+ if( d_free_vars.find( tn )==d_free_vars.end() ){
+ //if integer or real, make zero
+ if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
+ Rational z(0);
+ d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
+ }else{
+ if( d_type_map[ tn ].empty() ){
+ d_free_vars[tn] = NodeManager::currentNM()->mkVar( tn );
+ }else{
+ d_free_vars[tn] = d_type_map[ tn ][ 0 ];
+ }
+ }
+ }
+ return d_free_vars[tn];
+} \ No newline at end of file
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
new file mode 100644
index 000000000..5bf3d7900
--- /dev/null
+++ b/src/theory/quantifiers/term_database.h
@@ -0,0 +1,151 @@
+/**********************/
+/*! \file term_database.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 term database class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H
+#define __CVC4__QUANTIFIERS_TERM_DATABASE_H
+
+#include "theory/theory.h"
+
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+
+class TermArgTrie {
+private:
+ bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
+public:
+ /** the data */
+ std::map< Node, TermArgTrie > d_data;
+public:
+ bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
+};/* class TermArgTrie */
+
+class TermDb {
+ friend class ::CVC4::theory::QuantifiersEngine;
+private:
+ /** reference to the quantifiers engine */
+ QuantifiersEngine* d_quantEngine;
+ /** calculated no match terms */
+ bool d_matching_active;
+ /** terms processed */
+ std::map< Node, bool > d_processed;
+public:
+ TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}
+ ~TermDb(){}
+ /** map from APPLY_UF operators to ground terms for that operator */
+ std::map< Node, std::vector< Node > > d_op_map;
+ /** map from APPLY_UF functions to trie */
+ std::map< Node, TermArgTrie > d_func_map_trie;
+ /** map from APPLY_UF predicates to trie */
+ std::map< Node, TermArgTrie > d_pred_map_trie[2];
+ /** map from type nodes to terms of that type */
+ std::map< TypeNode, std::vector< Node > > d_type_map;
+ /** add a term to the database */
+ void addTerm( Node n, std::vector< Node >& added, bool withinQuant = false );
+ /** reset (calculate which terms are active) */
+ void reset( Theory::Effort effort );
+ /** set active */
+ void setMatchingActive( bool a ) { d_matching_active = a; }
+ /** get active */
+ bool getMatchingActive() { return d_matching_active; }
+public:
+ /** parent structure (for efficient E-matching):
+ n -> op -> index -> L
+ map from node "n" to a list of nodes "L", where each node n' in L
+ has operator "op", and n'["index"] = n.
+ for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }
+ */
+ std::map< Node, std::map< Node, std::map< int, std::vector< Node > > > > d_parents;
+private:
+ //map from types to model basis terms
+ std::map< TypeNode, Node > d_model_basis_term;
+ //map from ops to model basis terms
+ std::map< Node, Node > d_model_basis_op_term;
+ //map from instantiation terms to their model basis equivalent
+ std::map< Node, Node > d_model_basis;
+public:
+ //get model basis term
+ Node getModelBasisTerm( TypeNode tn, int i = 0 );
+ //get model basis term for op
+ Node getModelBasisOpTerm( Node op );
+ // compute model basis arg
+ void computeModelBasisArgAttribute( Node n );
+ //register instantiation terms with their corresponding model basis terms
+ void registerModelBasis( Node n, Node gn );
+ //get model basis
+ Node getModelBasis( Node n ) { return d_model_basis[n]; }
+private:
+ /** map from universal quantifiers to the list of variables */
+ std::map< Node, std::vector< Node > > d_vars;
+ /** map from universal quantifiers to the list of skolem constants */
+ std::map< Node, std::vector< Node > > d_skolem_constants;
+ /** map from universal quantifiers to their skolemized body */
+ std::map< Node, Node > d_skolem_body;
+ /** instantiation constants to universal quantifiers */
+ std::map< Node, Node > d_inst_constants_map;
+ /** map from universal quantifiers to their counterexample body */
+ std::map< Node, Node > d_counterexample_body;
+ /** free variable for instantiation constant type */
+ std::map< TypeNode, Node > d_free_vars;
+private:
+ /** make instantiation constants for */
+ void makeInstantiationConstantsFor( Node f );
+public:
+ /** map from universal quantifiers to the list of instantiation constants */
+ std::map< Node, std::vector< Node > > d_inst_constants;
+ /** set instantiation level attr */
+ void setInstantiationLevelAttr( Node n, uint64_t level );
+ /** set instantiation constant attr */
+ void setInstantiationConstantAttr( Node n, Node f );
+ /** get the i^th instantiation constant of f */
+ Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }
+ /** get number of instantiation constants for f */
+ int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); }
+ /** get the ce body f[e/x] */
+ Node getCounterexampleBody( Node f );
+ /** get the skolemized body f[e/x] */
+ Node getSkolemizedBody( Node f );
+ /** returns node n with bound vars of f replaced by instantiation constants of f
+ node n : is the futur pattern
+ node f : is the quantifier containing which bind the variable
+ return a pattern where the variable are replaced by variable for
+ instantiation.
+ */
+ Node getSubstitutedNode( Node n, Node f );
+ /** same as before but node f is just linked to the new pattern by the
+ applied attribute
+ vars the bind variable
+ nvars the same variable but with an attribute
+ */
+ Node convertNodeToPattern( Node n, Node f,
+ const std::vector<Node> & vars,
+ const std::vector<Node> & nvars);
+ /** get free variable for instantiation constant */
+ Node getFreeVariableForInstConstant( Node n );
+};/* class TermDb */
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index ead47e4b0..27310e21b 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -27,11 +27,7 @@
#include <map>
#include <time.h>
#include "theory/quantifiers/theory_quantifiers_instantiator.h"
-
-#define USE_FLIP_DECISION
-
-//static bool clockSet = false;
-//double initClock;
+#include "theory/quantifiers/term_database.h"
using namespace std;
using namespace CVC4;
@@ -45,11 +41,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
d_numRestarts(0){
d_numInstantiations = 0;
d_baseDecLevel = -1;
- if( Options::current()->finiteModelFind ){
- qe->addModule( new ModelEngine( this ) );
- }else{
- qe->addModule( new InstantiationEngine( this ) );
- }
}
@@ -65,10 +56,10 @@ void TheoryQuantifiers::addSharedTerm(TNode t) {
void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
Debug("quantifiers-other") << "TheoryQuantifiers::notifyEq(): "
<< lhs << " = " << rhs << endl;
-
+
}
-void TheoryQuantifiers::preRegisterTerm(TNode n) {
+void TheoryQuantifiers::preRegisterTerm(TNode n) {
Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){
getQuantifiersEngine()->registerQuantifier( n );
@@ -97,6 +88,10 @@ Node TheoryQuantifiers::getValue(TNode n) {
}
}
+void TheoryQuantifiers::collectModelInfo( TheoryModel* m ){
+
+}
+
void TheoryQuantifiers::check(Effort e) {
CodeTimer codeTimer(d_theoryTime);
@@ -119,7 +114,7 @@ void TheoryQuantifiers::check(Effort e) {
break;
}
}
- break;
+ break;
default:
Unhandled(assertion.getKind());
break;
@@ -147,7 +142,7 @@ void TheoryQuantifiers::assertExistential( Node n ){
Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
if( !n[0].hasAttribute(InstConstantAttribute()) ){
if( d_skolemized.find( n )==d_skolemized.end() ){
- Node body = getQuantifiersEngine()->getSkolemizedBody( n[0] );
+ Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] );
NodeBuilder<> nb(kind::OR);
nb << n[0] << body.notNode();
Node lem = nb;
@@ -159,9 +154,6 @@ void TheoryQuantifiers::assertExistential( Node n ){
}
bool TheoryQuantifiers::flipDecision(){
-#ifndef USE_FLIP_DECISION
- return false;
-#else
//Debug("quantifiers-flip") << "No instantiation given, flip decision, level = " << d_valuation.getDecisionLevel() << std::endl;
//for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
// Debug("quantifiers-flip") << " " << d_valuation.getDecision( i ) << std::endl;
@@ -179,7 +171,6 @@ bool TheoryQuantifiers::flipDecision(){
return restart();
}
return true;
-#endif
}
bool TheoryQuantifiers::restart(){
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 05c3b9695..517786400 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -34,6 +34,8 @@ namespace theory {
namespace quantifiers {
class TheoryEngine;
+class ModelEngine;
+class InstantiationEngine;
class TheoryQuantifiers : public Theory {
private:
@@ -59,6 +61,7 @@ public:
void check(Effort e);
void propagate(Effort level);
Node getValue(TNode n);
+ void collectModelInfo( TheoryModel* m );
void shutdown() { }
std::string identify() const { return std::string("TheoryQuantifiers"); }
bool flipDecision();
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
index a5b6cc3bc..84b6c65c7 100644
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
+++ b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
@@ -48,7 +48,7 @@ void InstantiatorTheoryQuantifiers::processResetInstantiationRound( Theory::Effo
}
-int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e, int limitInst ){
+int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e ){
Debug("quant-quant") << "Quant: Try to solve (" << e << ") for " << f << "... " << std::endl;
if( e<5 ){
return InstStrategy::STATUS_UNFINISHED;
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h
index 39e34c319..bf17495a1 100644
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.h
+++ b/src/theory/quantifiers/theory_quantifiers_instantiator.h
@@ -42,7 +42,7 @@ private:
/** reset instantiation */
void processResetInstantiationRound( Theory::Effort effort );
/** process at effort */
- int process( Node f, Theory::Effort effort, int e, int limitInst );
+ int process( Node f, Theory::Effort effort, int e );
class Statistics {
public:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback