summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/Makefile4
-rw-r--r--src/theory/quantifiers/Makefile.am21
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp393
-rw-r--r--src/theory/quantifiers/instantiation_engine.h79
-rw-r--r--src/theory/quantifiers/kinds48
-rw-r--r--src/theory/quantifiers/model_engine.cpp1401
-rw-r--r--src/theory/quantifiers/model_engine.h369
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp722
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h88
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp199
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h77
-rw-r--r--src/theory/quantifiers/theory_quantifiers_instantiator.cpp76
-rw-r--r--src/theory/quantifiers/theory_quantifiers_instantiator.h60
-rw-r--r--src/theory/quantifiers/theory_quantifiers_type_rules.h113
14 files changed, 3650 insertions, 0 deletions
diff --git a/src/theory/quantifiers/Makefile b/src/theory/quantifiers/Makefile
new file mode 100644
index 000000000..8ffdfb575
--- /dev/null
+++ b/src/theory/quantifiers/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/quantifiers
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
new file mode 100644
index 000000000..de74e44f8
--- /dev/null
+++ b/src/theory/quantifiers/Makefile.am
@@ -0,0 +1,21 @@
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libquantifiers.la
+
+libquantifiers_la_SOURCES = \
+ theory_quantifiers_type_rules.h \
+ theory_quantifiers.h \
+ quantifiers_rewriter.h \
+ quantifiers_rewriter.cpp \
+ theory_quantifiers.cpp \
+ theory_quantifiers_instantiator.h \
+ theory_quantifiers_instantiator.cpp \
+ instantiation_engine.h \
+ instantiation_engine.cpp \
+ model_engine.h \
+ model_engine.cpp
+
+EXTRA_DIST = kinds \ No newline at end of file
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
new file mode 100644
index 000000000..8478dff1e
--- /dev/null
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -0,0 +1,393 @@
+/********************* */
+/*! \file instantiation_engine.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 instantiation engine class
+ **/
+
+#include "theory/quantifiers/instantiation_engine.h"
+
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf_instantiator.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+//#define IE_PRINT_PROCESS_TIMES
+
+InstantiationEngine::InstantiationEngine( TheoryQuantifiers* th ) :
+d_th( th ){
+
+}
+
+QuantifiersEngine* InstantiationEngine::getQuantifiersEngine(){
+ return d_th->getQuantifiersEngine();
+}
+
+bool InstantiationEngine::hasAddedCbqiLemma( Node f ) {
+ return d_ce_lit.find( f ) != d_ce_lit.end();
+}
+
+void InstantiationEngine::addCbqiLemma( Node f ){
+ Assert( doCbqi( f ) && !hasAddedCbqiLemma( 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() );
+ //get the counterexample literal
+ Node ceBody = getQuantifiersEngine()->getCounterexampleBody( f );
+ Node ceLit = d_th->getValuation().ensureLiteral( ceBody.notNode() );
+ d_ce_lit[ f ] = ceLit;
+ getQuantifiersEngine()->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 );
+ 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 );
+}
+
+bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
+ //if counterexample-based quantifier instantiation is active
+ 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 );
+ if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
+ //add cbqi lemma
+ addCbqiLemma( f );
+ addedLemma = true;
+ }
+ }
+ if( addedLemma ){
+ return true;
+ }
+ }
+ //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
+ 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 );
+ //iterate over an internal effort level e
+ int e = 0;
+ int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
+ d_inst_round_status = InstStrategy::STATUS_UNFINISHED;
+ //while unfinished, try effort level=0,1,2....
+ while( d_inst_round_status==InstStrategy::STATUS_UNFINISHED && e<=eLimit ){
+ 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 );
+ 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;
+ 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 );
+ Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
+ InstStrategy::updateStatus( d_inst_round_status, quantStatus );
+ }
+ }
+ }
+ }
+ }
+ //do not consider another level if already added lemma at this level
+ if( getQuantifiersEngine()->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;
+ //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
+ if( !getQuantifiersEngine()->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");
+ 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
+ //flush lemmas to output channel
+ getQuantifiersEngine()->flushLemmas( &d_th->getOutputChannel() );
+ return true;
+ }
+}
+
+int ierCounter = 0;
+
+void InstantiationEngine::check( Theory::Effort e ){
+ if( e==Theory::EFFORT_FULL ){
+ ierCounter++;
+ }
+ //determine if we should perform check, based on instWhenMode
+ bool performCheck = false;
+ if( Options::current()->instWhenMode==Options::INST_WHEN_FULL ){
+ performCheck = ( e >= Theory::EFFORT_FULL );
+ }else if( Options::current()->instWhenMode==Options::INST_WHEN_FULL_LAST_CALL ){
+ performCheck = ( ( e==Theory::EFFORT_FULL && ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+ }else if( Options::current()->instWhenMode==Options::INST_WHEN_LAST_CALL ){
+ performCheck = ( e >= Theory::EFFORT_LAST_CALL );
+ }else{
+ performCheck = true;
+ }
+ 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
+ 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 ) {
+ for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
+ Node n = getQuantifiersEngine()->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 ) ){
+ active = value;
+ ceValue = true;
+ }else{
+ active = true;
+ }
+ getQuantifiersEngine()->setActive( n, active );
+ if( active ){
+ Debug("quantifiers") << " Active : " << n;
+ quantActive = true;
+ }else{
+ Debug("quantifiers") << " NOT active : " << n;
+ if( d_th->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 ) );
+ }
+ if( d_th->getValuation().hasSatValue( n, value ) ){
+ Debug("quantifiers") << ", value = " << value;
+ }
+ if( ceValue ){
+ Debug("quantifiers") << ", ce is asserted";
+ }
+ Debug("quantifiers") << std::endl;
+ }else{
+ getQuantifiersEngine()->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;
+ }
+ //}
+ if( quantActive ){
+ bool addedLemmas = doInstantiationRound( e );
+ //Debug("quantifiers-dec") << "Do instantiation, level = " << d_th->getValuation().getDecisionLevel() << std::endl;
+ //for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
+ // Debug("quantifiers-dec") << " " << d_valuation.getDecision( i ) << std::endl;
+ //}
+ if( e==Theory::EFFORT_LAST_CALL ){
+ if( !addedLemmas ){
+ if( d_inst_round_status==InstStrategy::STATUS_SAT ){
+ Debug("inst-engine") << "No instantiation given, returning SAT..." << std::endl;
+ debugSat( SAT_INST_STRATEGY );
+ }else{
+ Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl;
+ d_th->getOutputChannel().setIncomplete();
+ }
+ }
+ }
+ }else{
+ if( e==Theory::EFFORT_LAST_CALL ){
+ if( Options::current()->cbqi ){
+ debugSat( SAT_CBQI );
+ }
+ }
+ }
+#ifdef IE_PRINT_PROCESS_TIMES
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Notice() << "Done Run instantiation round " << (clSet2-clSet) << std::endl;
+#endif
+ }
+}
+
+void InstantiationEngine::registerQuantifier( Node f ){
+ //Notice() << "do cbqi " << f << " ? " << std::endl;
+ Node ceBody = getQuantifiersEngine()->getCounterexampleBody( f );
+ if( !doCbqi( f ) ){
+ getQuantifiersEngine()->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 );
+ }
+
+ //take into account user patterns
+ if( f.getNumChildren()==3 ){
+ Node subsPat = getQuantifiersEngine()->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] );
+ }
+ }
+}
+
+void InstantiationEngine::assertNode( Node f ){
+ ////if we are doing cbqi and have not added the lemma yet, do so
+ //if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
+ // addCbqiLemma( f );
+ //}
+}
+
+bool InstantiationEngine::hasApplyUf( Node f ){
+ if( f.getKind()==APPLY_UF ){
+ return true;
+ }else{
+ for( int i=0; i<(int)f.getNumChildren(); i++ ){
+ if( hasApplyUf( f[i] ) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+bool InstantiationEngine::hasNonArithmeticVariable( Node f ){
+ for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+ TypeNode tn = f[0][i].getType();
+ if( !tn.isInteger() && !tn.isReal() ){
+ return true;
+ }
+ }
+ return false;
+}
+
+bool InstantiationEngine::doCbqi( Node f ){
+ if( Options::current()->cbqiSetByUser ){
+ return Options::current()->cbqi;
+ }else if( Options::current()->cbqi ){
+ //if quantifier has a non-arithmetic variable, then do not use cbqi
+ //if quantifier has an APPLY_UF term, then do not use cbqi
+ return !hasNonArithmeticVariable( f ) && !hasApplyUf( f[1] );
+ }else{
+ return false;
+ }
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+//void InstantiationEngine::registerLiterals( Node n, Node f ){
+// if( n.getAttribute(InstConstantAttribute())==f ){
+// for( int i=0; i<(int)n.getNumChildren(); i++ ){
+// registerLiterals( n[i], f );
+// }
+// if( !d_ce_lit[ f ].isNull() ){
+// if( getQuantifiersEngine()->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 );
+// }
+// }
+// }
+// }
+//}
+
+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( 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 );
+ Node cel = d_ce_lit[ f ];
+ Assert( !cel.isNull() );
+ bool value;
+ if( d_th->getValuation().hasSatValue( cel, value ) ){
+ if( !value ){
+ AlwaysAssert(! d_th->getValuation().isDecision( cel ),
+ "bad decision on counterexample literal");
+ }
+ }
+ }
+ //}
+ Debug("quantifiers-sat") << "return SAT: Cbqi, no quantifier is active. " << std::endl;
+ //static bool setTrust = false;
+ //if( !setTrust ){
+ // setTrust = true;
+ // Notice() << "trust-";
+ //}
+ }else if( reason==SAT_INST_STRATEGY ){
+ Debug("quantifiers-sat") << "return SAT: No strategy chose to add an instantiation." << std::endl;
+ //Notice() << "sat ";
+ //Unimplemented();
+ }
+}
+
+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 not already set, propagate as decision
+ d_th->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
new file mode 100644
index 000000000..c6aaed18a
--- /dev/null
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -0,0 +1,79 @@
+/********************* */
+/*! \file instantiation_engine.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 Instantiation Engine classes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INSTANTIATION_ENGINE_H
+#define __CVC4__INSTANTIATION_ENGINE_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/theory_quantifiers.h"
+
+namespace CVC4 {
+namespace theory {
+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;
+private:
+ bool hasAddedCbqiLemma( Node f );
+ void addCbqiLemma( Node f );
+private:
+ /** helper functions */
+ bool hasNonArithmeticVariable( Node f );
+ bool hasApplyUf( Node f );
+ /** whether to do CBQI for quantifier f */
+ bool doCbqi( Node f );
+private:
+ /** do instantiation round */
+ bool doInstantiationRound( Theory::Effort effort );
+ /** register literals of n, f is the quantifier it belongs to */
+ //void registerLiterals( Node n, Node f );
+private:
+ enum{
+ SAT_CBQI,
+ SAT_INST_STRATEGY,
+ };
+ /** debug sat */
+ void debugSat( int reason );
+public:
+ InstantiationEngine( TheoryQuantifiers* th );
+ ~InstantiationEngine(){}
+
+ void check( Theory::Effort e );
+ void registerQuantifier( Node f );
+ void assertNode( Node f );
+ Node explain(TNode n){ return Node::null(); }
+ void propagate( Theory::Effort level );
+public:
+ /** get the corresponding counterexample literal for quantified formula node n */
+ Node getCounterexampleLiteralFor( Node f ) { return d_ce_lit.find( f )==d_ce_lit.end() ? Node::null() : d_ce_lit[ f ]; }
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
new file mode 100644
index 000000000..106d95cef
--- /dev/null
+++ b/src/theory/quantifiers/kinds
@@ -0,0 +1,48 @@
+# kinds -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
+typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
+instantiator ::CVC4::theory::quantifiers::InstantiatorTheoryQuantifiers "theory/quantifiers/theory_quantifiers_instantiator.h"
+
+properties check propagate presolve
+
+rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
+
+operator FORALL 2:3 "universally quantified formula"
+
+operator EXISTS 2:3 "existentially quantified formula"
+
+variable INST_CONSTANT "instantiation constant"
+
+sort BOUND_VAR_LIST_TYPE \
+ Cardinality::INTEGERS \
+ not-well-founded \
+ "Bound Var type"
+
+operator BOUND_VAR_LIST 1: "bound variables"
+
+sort INST_PATTERN_TYPE \
+ Cardinality::INTEGERS \
+ not-well-founded \
+ "Instantiation pattern type"
+
+operator INST_PATTERN 1: "instantiation pattern"
+
+sort INST_PATTERN_LIST_TYPE \
+ Cardinality::INTEGERS \
+ not-well-founded \
+ "Instantiation pattern list type"
+
+operator INST_PATTERN_LIST 1: "instantiation pattern list"
+
+typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule
+typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule
+typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule
+typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
+typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule
+
+endtheory
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
new file mode 100644
index 000000000..a72b103d1
--- /dev/null
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -0,0 +1,1401 @@
+/********************* */
+/*! \file model_engine.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 class
+ **/
+
+#include "theory/quantifiers/model_engine.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"
+
+//#define ME_PRINT_PROCESS_TIMES
+
+//#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
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+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 );
+ }
+}
+
+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 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] ] );
+ }
+ 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;
+ }
+ }else{
+ //argument is not a defined argument: thus, it depends on this argument
+ childDepIndex[i] = argIndex+1;
+ }
+ }
+ //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;
+ }else{
+ defaultVal = Node::null();
+ }
+ }
+ }
+ //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 );
+ }else{
+ it->second.simplify( op, defaultVal, argIndex+1 );
+ }
+ }
+ }
+ 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 );
+ }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 );
+ }
+ }
+ 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;
+ }
+}
+
+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;
+ }
+ }
+ }
+ 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( 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;
+ }
+ }
+}
+
+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();
+ }
+ 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();
+ }
+}
+
+bool UfModel::isConstant(){
+ Node gn = d_me->getModelBasisApplyUfTerm( d_op );
+ Node n = getConstantValue( d_me->getQuantifiersEngine(), gn );
+ return !n.isNull();
+}
+
+void UfModel::buildModel(){
+#ifdef RECONSIDER_FUNC_CONSTANT
+ if( d_model_constructed ){
+ if( d_reconsider_model ){
+ //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();
+ }
+ }
+ }
+#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 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 );
+ 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;
+ }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] << " ";
+ }
+ 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 );
+ Debug("fmf-model-cons") << " Making model...";
+ setModel();
+ Debug("fmf-model-cons") << " Finished constructing model for " << d_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 );
+ }
+}
+
+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();
+}
+
+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;
+
+ 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;
+ // }
+ // }
+ // }
+ //}
+}
+
+//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();
+}
+
+void ModelEngine::check( Theory::Effort e ){
+ if( e==Theory::EFFORT_LAST_CALL ){
+ bool quantsInit = true;
+ //first, check if we can minimize the model further
+ if( !d_ss->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;
+ }
+ }
+ }
+ if( quantsInit ){
+#ifdef ME_PRINT_PROCESS_TIMES
+ Notice() << "---Instantiation Round---" << std::endl;
+#endif
+ 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();
+ }
+ }
+ //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 );
+ }
+ }
+#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() );
+ }
+}
+
+void ModelEngine::registerQuantifier( Node f ){
+
+}
+
+void ModelEngine::assertNode( Node f ){
+
+}
+
+bool ModelEngine::useModel() {
+ return Options::current()->fmfModelBasedInst;
+}
+
+bool 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
+ // 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 ){
+ // Node n = it->first;
+ // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){
+ // Notice() << "Unhandled phase req: " << n << std::endl;
+ // }
+ //}
+
+ std::vector< Node > terms;
+ for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+ terms.push_back( getModelBasisTerm( f[0][j].getType() ) );
+ }
+ ++(d_statistics.d_num_quants_init);
+ if( d_quantEngine->addInstantiation( f, terms ) ){
+ return false;
+ }else{
+ //usually shouldn't happen
+ //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
+ }
+}
+
+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 addedLemmas = 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") << 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() ){
+#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;
+ }
+ }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;
+ }
+ }
+ }
+ 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;
+ }
+ }
+ }
+ Debug("fmf-model-eval-debug") << "Evaluate literal: return " << retVal << ", depends = " << maxIndex << std::endl;
+ depIndex = maxIndex;
+ }
+ 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() );
+ }
+ return val;
+ }
+ }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 );
+}
+
+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 );
+ Debug( c ) << " ";
+ if( d_quant_sat.find( f )!=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;
+ }
+}
+
+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 ),
+ d_num_quants_init("ModelEngine::Num_Quants", 0 ),
+ 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);
+ StatisticsRegistry::registerStat(&d_num_quants_init);
+ StatisticsRegistry::registerStat(&d_num_quants_init_fail);
+}
+
+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
new file mode 100644
index 000000000..4031efdf9
--- /dev/null
+++ b/src/theory/quantifiers/model_engine.h
@@ -0,0 +1,369 @@
+/********************* */
+/*! \file instantiation_engine.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 Instantiation Engine classes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MODEL_ENGINE_H
+#define __CVC4__MODEL_ENGINE_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/theory_quantifiers.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace uf{
+ class StrongSolverTheoryUf;
+}
+
+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
+{
+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 );
+};
+
+
+
+
+class ModelEngine : public QuantifiersModule
+{
+ friend class UfModel;
+ friend class RepAlphabetIterator;
+private:
+ TheoryQuantifiers* d_th;
+ QuantifiersEngine* d_quantEngine;
+ uf::StrongSolverTheoryUf* d_ss;
+ //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:
+ 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;
+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 );
+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 );
+public:
+ ModelEngine( TheoryQuantifiers* th );
+ ~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 );
+ void assertNode( Node f );
+ Node explain(TNode n){ return Node::null(); }
+ void propagate( Theory::Effort level ){}
+ void debugPrint( const char* c );
+public:
+ /** statistics class */
+ 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;
+ IntStat d_num_quants_init;
+ IntStat d_num_quants_init_fail;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
new file mode 100644
index 000000000..0fba9d59e
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -0,0 +1,722 @@
+/********************* */
+/*! \file theory_quantifiers_rewriter.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 QuantifiersRewriter class
+ **/
+
+#include "theory/quantifiers/quantifiers_rewriter.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 QuantifiersRewriter::isClause( Node n ){
+ if( isLiteral( n ) ){
+ return true;
+ }else if( n.getKind()==NOT ){
+ return isCube( n[0] );
+ }else if( n.getKind()==OR ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( !isClause( n[i] ) ){
+ return false;
+ }
+ }
+ return true;
+ }else if( n.getKind()==IMPLIES ){
+ return isCube( n[0] ) && isClause( n[1] );
+ }else{
+ return false;
+ }
+}
+
+bool QuantifiersRewriter::isLiteral( Node n ){
+ switch( n.getKind() ){
+ case NOT:
+ return isLiteral( n[0] );
+ break;
+ case OR:
+ case AND:
+ case IMPLIES:
+ case XOR:
+ case ITE:
+ case IFF:
+ return false;
+ break;
+ case EQUAL:
+ return n[0].getType()!=NodeManager::currentNM()->booleanType();
+ break;
+ default:
+ break;
+ }
+ return true;
+}
+
+bool QuantifiersRewriter::isCube( Node n ){
+ if( isLiteral( n ) ){
+ return true;
+ }else if( n.getKind()==NOT ){
+ return isClause( n[0] );
+ }else if( n.getKind()==AND ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( !isCube( n[i] ) ){
+ return false;
+ }
+ }
+ return true;
+ }else{
+ return false;
+ }
+}
+
+void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
+ if( n.getKind()==OR ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ t << n[i];
+ }
+ }else{
+ t << n;
+ }
+}
+
+void QuantifiersRewriter::computeArgs( std::map< Node, bool >& active, Node n ){
+ if( active.find( n )!=active.end() ){
+ active[n] = true;
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ computeArgs( active, n[i] );
+ }
+ }
+}
+
+void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ){
+ std::map< Node, bool > active;
+ for( int i=0; i<(int)args.size(); i++ ){
+ active[ args[i] ] = false;
+ }
+ //Notice() << "For " << n << " : " << std::endl;
+ computeArgs( active, n );
+ activeArgs.clear();
+ for( std::map< Node, bool >::iterator it = active.begin(); it != active.end(); ++it ){
+ Node n = it->first;
+ //Notice() << " " << it->first << " is " << it->second << std::endl;
+ if( it->second ){ //only add bound variables that occur in body
+ activeArgs.push_back( it->first );
+ }
+ }
+}
+
+bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
+ if( std::find( args.begin(), args.end(), n )!=args.end() ){
+ return true;
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( hasArg( args, n[i] ) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){
+ if( n.getKind()==FORALL || n.getKind()==EXISTS ){
+ Debug("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
+ NestedQuantAttribute nqai;
+ n.setAttribute(nqai,q);
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ setNestedQuantifiers( n[i], q );
+ }
+}
+
+RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
+ Debug("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
+ if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
+ if( !in.hasAttribute(NestedQuantAttribute()) ){
+ setNestedQuantifiers( in[ 1 ], in );
+ }
+ std::vector< Node > args;
+ for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
+ args.push_back( in[0][i] );
+ }
+ Node body = in[1];
+ bool doRewrite = false;
+ while( body.getNumChildren()>=2 && body.getKind()==in.getKind() ){
+ for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+ args.push_back( body[0][i] );
+ }
+ body = body[1];
+ doRewrite = true;
+ }
+ if( doRewrite ){
+ std::vector< Node > children;
+ children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
+ children.push_back( body );
+ if( in.getNumChildren()==3 ){
+ children.push_back( in[2] );
+ }
+ Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
+ if( in!=n ){
+ if( in.hasAttribute(NestedQuantAttribute()) ){
+ setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
+ }
+ Debug("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
+ Debug("quantifiers-pre-rewrite") << " to " << std::endl;
+ Debug("quantifiers-pre-rewrite") << n << std::endl;
+ }
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+ }
+ return RewriteResponse(REWRITE_DONE, in);
+}
+
+RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
+ Debug("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
+ if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
+ //get the arguments
+ std::vector< Node > args;
+ for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
+ args.push_back( in[0][i] );
+ }
+ //get the body
+ Node body = in[1];
+ if( in.getKind()==EXISTS ){
+ body = body.getKind()==NOT ? body[0] : body.notNode();
+ }
+ //get the instantiation pattern list
+ Node ipl;
+ if( in.getNumChildren()==3 ){
+ ipl = in[2];
+ }
+ bool isNested = in.hasAttribute(NestedQuantAttribute());
+ //compute miniscoping first
+ Node n = body;//computeNNF( body ); TODO: compute NNF here (current bad idea since arithmetic rewrites equalities)
+ if( body!=n ){
+ Notice() << "NNF " << body << " -> " << n << std::endl;
+ }
+ n = computeMiniscoping( args, n, ipl, isNested );
+ if( in.getKind()==kind::EXISTS ){
+ n = n.getKind()==NOT ? n[0] : n.notNode();
+ }
+ //compute other rewrite options for each produced quantifier
+ n = rewriteQuants( n, isNested, true );
+ //print if changed
+ if( in!=n ){
+ if( in.hasAttribute(NestedQuantAttribute()) ){
+ setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
+ }
+ Debug("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
+ Debug("quantifiers-rewrite") << " to " << std::endl;
+ Debug("quantifiers-rewrite") << n << std::endl;
+ if( in.hasAttribute(InstConstantAttribute()) ){
+ InstConstantAttribute ica;
+ n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
+ }
+ }
+ return RewriteResponse(REWRITE_DONE, n );
+ }
+ return RewriteResponse(REWRITE_DONE, in);
+}
+
+Node QuantifiersRewriter::computeNNF( Node body ){
+ if( body.getKind()==NOT ){
+ if( body[0].getKind()==NOT ){
+ return computeNNF( body[0][0] );
+ }else if( isLiteral( body[0] ) ){
+ return body;
+ }else{
+ std::vector< Node > children;
+ Kind k = body[0].getKind();
+ if( body[0].getKind()==OR || body[0].getKind()==IMPLIES || body[0].getKind()==AND ){
+ for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+ Node nn = body[0].getKind()==IMPLIES && i==0 ? body[0][i] : body[0][i].notNode();
+ children.push_back( computeNNF( nn ) );
+ }
+ k = body[0].getKind()==AND ? OR : AND;
+ }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){
+ for( int i=0; i<2; i++ ){
+ Node nn = i==0 ? body[0][i] : body[0][i].notNode();
+ children.push_back( computeNNF( nn ) );
+ }
+ }else if( body[0].getKind()==ITE ){
+ for( int i=0; i<3; i++ ){
+ Node nn = i==0 ? body[0][i] : body[0][i].notNode();
+ children.push_back( computeNNF( nn ) );
+ }
+ }else{
+ Notice() << "Unhandled Quantifiers NNF: " << body << std::endl;
+ return body;
+ }
+ return NodeManager::currentNM()->mkNode( k, children );
+ }
+ }else if( isLiteral( body ) ){
+ return body;
+ }else{
+ std::vector< Node > children;
+ bool childrenChanged = false;
+ for( int i=0; i<(int)body.getNumChildren(); i++ ){
+ Node nc = computeNNF( body[i] );
+ children.push_back( nc );
+ childrenChanged = childrenChanged || nc!=body[i];
+ }
+ if( childrenChanged ){
+ return NodeManager::currentNM()->mkNode( body.getKind(), children );
+ }else{
+ return body;
+ }
+ }
+}
+
+Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
+ //Notice() << "Compute var elimination for " << f << std::endl;
+ std::map< Node, bool > litPhaseReq;
+ QuantifiersEngine::computePhaseReqs( body, false, litPhaseReq );
+ std::vector< Node > vars;
+ std::vector< Node > subs;
+ for( std::map< Node, bool >::iterator it = litPhaseReq.begin(); it != litPhaseReq.end(); ++it ){
+ //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
+ if( it->first.getKind()==EQUAL ){
+ if( it->second ){
+ for( int i=0; i<2; i++ ){
+ int j = i==0 ? 1 : 0;
+ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
+ if( ita!=args.end() ){
+ std::vector< Node > temp;
+ temp.push_back( it->first[i] );
+ if( !hasArg( temp, it->first[j] ) ){
+ vars.push_back( it->first[i] );
+ subs.push_back( it->first[j] );
+ args.erase( ita );
+ break;
+ }
+ }
+ }
+ if( !vars.empty() ){
+ break;
+ }
+ }
+ }
+ }
+ if( !vars.empty() ){
+ //Notice() << "VE " << vars.size() << "/" << n[0].getNumChildren() << std::endl;
+ //remake with eliminated nodes
+ body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ body = Rewriter::rewrite( body );
+ if( !ipl.isNull() ){
+ ipl = ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ }
+ }
+ return body;
+}
+
+Node QuantifiersRewriter::computeClause( Node n ){
+ Assert( isClause( n ) );
+ if( isLiteral( n ) ){
+ return n;
+ }else{
+ NodeBuilder<> t(OR);
+ if( n.getKind()==NOT ){
+ if( n[0].getKind()==NOT ){
+ return computeClause( n[0][0] );
+ }else{
+ //De-Morgan's law
+ Assert( n[0].getKind()==AND );
+ for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
+ Node nn = computeClause( n[0][i].notNode() );
+ addNodeToOrBuilder( nn, t );
+ }
+ }
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ Node nc = ( ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i] );
+ Node nn = computeClause( nc );
+ addNodeToOrBuilder( nn, t );
+ }
+ }
+ return t.constructNode();
+ }
+}
+
+Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){
+ if( isLiteral( n ) ){
+ return n;
+ }else if( !forcePred && isClause( n ) ){
+ return computeClause( n );
+ }else{
+ Kind k = ( n.getKind()==IMPLIES ? OR : ( n.getKind()==XOR ? IFF : n.getKind() ) );
+ NodeBuilder<> t(k);
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ Node nc = ( i==0 && ( n.getKind()==IMPLIES || n.getKind()==XOR ) ) ? n[i].notNode() : n[i];
+ Node ncnf = computeCNF( nc, args, defs, k!=OR );
+ if( k==OR ){
+ addNodeToOrBuilder( ncnf, t );
+ }else{
+ t << ncnf;
+ }
+ }
+ if( !forcePred && k==OR ){
+ return t.constructNode();
+ }else{
+ //compute the free variables
+ Node nt = t;
+ std::vector< Node > activeArgs;
+ computeArgs( args, activeArgs, nt );
+ std::vector< TypeNode > argTypes;
+ for( int i=0; i<(int)activeArgs.size(); i++ ){
+ argTypes.push_back( activeArgs[i].getType() );
+ }
+ //create the predicate
+ Assert( argTypes.size()>0 );
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() );
+ std::stringstream ss;
+ ss << "cnf_" << n.getKind() << "_" << n.getId();
+ Node op = NodeManager::currentNM()->mkVar( ss.str(), typ );
+ std::vector< Node > predArgs;
+ predArgs.push_back( op );
+ predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() );
+ Node pred = NodeManager::currentNM()->mkNode( APPLY_UF, predArgs );
+ Debug("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl;
+ //create the bound var list
+ Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, activeArgs );
+ //now, look at the structure of nt
+ if( nt.getKind()==NOT ){
+ //case for NOT
+ for( int i=0; i<2; i++ ){
+ NodeBuilder<> tt(OR);
+ tt << ( i==0 ? nt[0].notNode() : nt[0] );
+ tt << ( i==0 ? pred.notNode() : pred );
+ defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
+ }
+ }else if( nt.getKind()==OR ){
+ //case for OR
+ for( int i=0; i<(int)nt.getNumChildren(); i++ ){
+ NodeBuilder<> tt(OR);
+ tt << nt[i].notNode() << pred;
+ defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
+ }
+ NodeBuilder<> tt(OR);
+ for( int i=0; i<(int)nt.getNumChildren(); i++ ){
+ tt << nt[i];
+ }
+ tt << pred.notNode();
+ defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
+ }else if( nt.getKind()==AND ){
+ //case for AND
+ for( int i=0; i<(int)nt.getNumChildren(); i++ ){
+ NodeBuilder<> tt(OR);
+ tt << nt[i] << pred.notNode();
+ defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
+ }
+ NodeBuilder<> tt(OR);
+ for( int i=0; i<(int)nt.getNumChildren(); i++ ){
+ tt << nt[i].notNode();
+ }
+ tt << pred;
+ defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
+ }else if( nt.getKind()==IFF ){
+ //case for IFF
+ for( int i=0; i<4; i++ ){
+ NodeBuilder<> tt(OR);
+ tt << ( ( i==0 || i==3 ) ? nt[0].notNode() : nt[0] );
+ tt << ( ( i==1 || i==3 ) ? nt[1].notNode() : nt[1] );
+ tt << ( ( i==0 || i==1 ) ? pred.notNode() : pred );
+ defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
+ }
+ }else if( nt.getKind()==ITE ){
+ //case for ITE
+ for( int j=1; j<=2; j++ ){
+ for( int i=0; i<2; i++ ){
+ NodeBuilder<> tt(OR);
+ tt << ( ( j==1 ) ? nt[0].notNode() : nt[0] );
+ tt << ( ( i==1 ) ? nt[j].notNode() : nt[j] );
+ tt << ( ( i==0 ) ? pred.notNode() : pred );
+ defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
+ }
+ }
+ for( int i=0; i<2; i++ ){
+ NodeBuilder<> tt(OR);
+ tt << ( i==0 ? nt[1].notNode() : nt[1] );
+ tt << ( i==0 ? nt[2].notNode() : nt[2] );
+ tt << ( i==1 ? pred.notNode() : pred );
+ defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
+ }
+ }else{
+ Notice() << "Unhandled Quantifiers CNF: " << nt << std::endl;
+ }
+ return pred;
+ }
+ }
+}
+
+Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq ){
+ if( body.getKind()==FORALL ){
+ if( pol==polReq ){
+ std::vector< Node > terms;
+ std::vector< Node > subs;
+ if( polReq ){
+ //for doing prenexing of same-signed quantifiers
+ //must rename each variable that already exists
+ for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+ //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
+ terms.push_back( body[0][i] );
+ subs.push_back( NodeManager::currentNM()->mkVar( body[0][i].getType() ) );
+ }
+ args.insert( args.end(), subs.begin(), subs.end() );
+ }else{
+ std::vector< TypeNode > argTypes;
+ for( int i=0; i<(int)args.size(); i++ ){
+ argTypes.push_back( args[i].getType() );
+ }
+ //for doing pre-skolemization of opposite-signed quantifiers
+ for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+ terms.push_back( body[0][i] );
+ //make the new function symbol
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, body[0][i].getType() );
+ Node op = NodeManager::currentNM()->mkVar( typ );
+ std::vector< Node > funcArgs;
+ funcArgs.push_back( op );
+ funcArgs.insert( funcArgs.end(), args.begin(), args.end() );
+ subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, funcArgs ) );
+ }
+ }
+ Node newBody = body[1];
+ newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+ return newBody;
+ }else{
+ return body;
+ }
+ }else if( body.getKind()==ITE || body.getKind()==XOR || body.getKind()==IFF ){
+ return body;
+ }else{
+ Assert( body.getKind()!=EXISTS );
+ bool childrenChanged = false;
+ std::vector< Node > newChildren;
+ for( int i=0; i<(int)body.getNumChildren(); i++ ){
+ bool newPol = ( body.getKind()==NOT || ( body.getKind()==IMPLIES && i==0 ) ) ? !pol : pol;
+ Node n = computePrenex( body[i], args, newPol, polReq );
+ newChildren.push_back( n );
+ if( n!=body[i] ){
+ childrenChanged = true;
+ }
+ }
+ if( childrenChanged ){
+ if( body.getKind()==NOT && newChildren[0].getKind()==NOT ){
+ return newChildren[0][0];
+ }else{
+ return NodeManager::currentNM()->mkNode( body.getKind(), newChildren );
+ }
+ }else{
+ return body;
+ }
+ }
+}
+
+//general method for computing various rewrites
+Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
+ std::vector< Node > args;
+ for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+ args.push_back( f[0][i] );
+ }
+ NodeBuilder<> defs(kind::AND);
+ Node n = f[1];
+ Node ipl;
+ if( f.getNumChildren()==3 ){
+ ipl = f[2];
+ }
+ if( computeOption==COMPUTE_NNF ){
+ n = computeNNF( n );
+ }else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){
+ n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX );
+ }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
+ Node prev;
+ do{
+ prev = n;
+ n = computeVarElimination( n, args, ipl );
+ }while( prev!=n && !args.empty() );
+ }else if( computeOption==COMPUTE_CNF ){
+ //n = computeNNF( n );
+ n = computeCNF( n, args, defs, false );
+ ipl = Node::null();
+ }
+ if( f[1]==n && args.size()==long(f[0].getNumChildren()) ){
+ return f;
+ }else{
+ if( args.empty() ){
+ defs << n;
+ }else{
+ std::vector< Node > children;
+ children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
+ children.push_back( n );
+ if( !ipl.isNull() ){
+ children.push_back( ipl );
+ }
+ defs << NodeManager::currentNM()->mkNode(kind::FORALL, children );
+ }
+ return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode();
+ }
+}
+
+Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
+ std::vector< Node > activeArgs;
+ computeArgs( args, activeArgs, body );
+ if( activeArgs.empty() ){
+ return body;
+ }else{
+ std::vector< Node > children;
+ children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) );
+ children.push_back( body );
+ if( !ipl.isNull() ){
+ children.push_back( ipl );
+ }
+ return NodeManager::currentNM()->mkNode( kind::FORALL, children );
+ }
+}
+
+Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested ){
+ //Notice() << "rewrite quant " << body << std::endl;
+ if( body.getKind()==FORALL ){
+ //combine arguments
+ std::vector< Node > newArgs;
+ for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+ newArgs.push_back( body[0][i] );
+ }
+ newArgs.insert( newArgs.end(), args.begin(), args.end() );
+ return mkForAll( newArgs, body[ 1 ], ipl );
+ }else if( !isNested ){
+ if( body.getKind()==NOT ){
+ //push not downwards
+ if( body[0].getKind()==NOT ){
+ return computeMiniscoping( args, body[0][0], ipl );
+ }else if( body[0].getKind()==AND ){
+ if( doMiniscopingNoFreeVar() ){
+ NodeBuilder<> t(kind::OR);
+ for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+ t << ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() );
+ }
+ return computeMiniscoping( args, t.constructNode(), ipl );
+ }
+ }else if( body[0].getKind()==OR || body[0].getKind()==IMPLIES ){
+ if( doMiniscopingAnd() ){
+ NodeBuilder<> t(kind::AND);
+ for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+ Node trm = ( body[0].getKind()==IMPLIES && i==0 ) ? body[0][i] : ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() );
+ t << computeMiniscoping( args, trm, ipl );
+ }
+ return t.constructNode();
+ }
+ }
+ }else if( body.getKind()==AND ){
+ if( doMiniscopingAnd() ){
+ //break apart
+ NodeBuilder<> t(kind::AND);
+ for( int i=0; i<(int)body.getNumChildren(); i++ ){
+ t << computeMiniscoping( args, body[i], ipl );
+ }
+ Node retVal = t;
+ return retVal;
+ }
+ }else if( body.getKind()==OR || body.getKind()==IMPLIES ){
+ if( doMiniscopingNoFreeVar() ){
+ Node newBody = body;
+ NodeBuilder<> body_split(kind::OR);
+ NodeBuilder<> tb(kind::OR);
+ for( int i=0; i<(int)body.getNumChildren(); i++ ){
+ Node trm = ( body.getKind()==IMPLIES && i==0 ) ? ( body[i].getKind()==NOT ? body[i][0] : body[i].notNode() ) : body[i];
+ if( hasArg( args, body[i] ) ){
+ tb << trm;
+ }else{
+ body_split << trm;
+ }
+ }
+ if( tb.getNumChildren()==0 ){
+ return body_split;
+ }else if( body_split.getNumChildren()>0 ){
+ newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
+ body_split << mkForAll( args, newBody, ipl );
+ return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
+ }
+ }
+ }
+ }
+ return mkForAll( args, body, ipl );
+}
+
+Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested, bool duringRewrite ){
+ if( n.getKind()==FORALL ){
+ return rewriteQuant( n, isNested, duringRewrite );
+ }else if( isLiteral( n ) ){
+ return n;
+ }else{
+ NodeBuilder<> tt(n.getKind());
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ tt << rewriteQuants( n[i], isNested, duringRewrite );
+ }
+ return tt.constructNode();
+ }
+}
+
+Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrite ){
+ Node prev = n;
+ for( int op=0; op<COMPUTE_LAST; op++ ){
+ if( doOperation( n, isNested, op, duringRewrite ) ){
+ Node prev2 = n;
+ n = computeOperation( n, op );
+ if( prev2!=n ){
+ Debug("quantifiers-rewrite-op") << "Rewrite op " << op << ": rewrite " << prev2 << std::endl;
+ Debug("quantifiers-rewrite-op") << " to " << std::endl;
+ Debug("quantifiers-rewrite-op") << n << std::endl;
+ }
+ }
+ }
+ if( prev==n ){
+ return n;
+ }else{
+ //rewrite again until fix point is reached
+ return rewriteQuant( n, isNested, duringRewrite );
+ }
+}
+
+bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
+ return Options::current()->miniscopeQuantFreeVar;
+}
+
+bool QuantifiersRewriter::doMiniscopingAnd(){
+ if( Options::current()->miniscopeQuant ){
+ return true;
+ }else{
+ if( Options::current()->cbqi ){
+ return true;
+ }else{
+ return false;
+ }
+ }
+}
+
+bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, bool duringRewrite ){
+ if( computeOption==COMPUTE_NNF ){
+ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
+ }else if( computeOption==COMPUTE_PRE_SKOLEM ){
+ return Options::current()->preSkolemQuant && !duringRewrite;
+ }else if( computeOption==COMPUTE_PRENEX ){
+ return Options::current()->prenexQuant;
+ }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
+ return Options::current()->varElimQuant;
+ }else if( computeOption==COMPUTE_CNF ){
+ return Options::current()->cnfQuant && !duringRewrite;// || Options::current()->finiteModelFind;
+ }else{
+ return false;
+ }
+}
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
new file mode 100644
index 000000000..8c037d30b
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -0,0 +1,88 @@
+/********************* */
+/*! \file quantifiers_rewriter.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** 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 Rewriter for the theory of inductive quantifiers
+ **
+ ** Rewriter for the theory of inductive quantifiers.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+
+#include "theory/rewriter.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+// attribute for "contains instantiation constants from"
+struct NestedQuantAttributeId {};
+typedef expr::Attribute<NestedQuantAttributeId, Node> NestedQuantAttribute;
+
+class QuantifiersRewriter {
+public:
+ static bool isClause( Node n );
+ static bool isLiteral( Node n );
+ static bool isCube( Node n );
+private:
+ static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
+ static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
+ static void computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
+ static bool hasArg( std::vector< Node >& args, Node n );
+ static void setNestedQuantifiers( Node n, Node q );
+ static void computeArgs( std::map< Node, bool >& active, Node n );
+ static Node computeClause( Node n );
+private:
+ static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
+ static Node computeNNF( Node body );
+ static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
+ static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
+ static Node computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq );
+private:
+ enum{
+ COMPUTE_NNF = 0,
+ COMPUTE_PRE_SKOLEM,
+ COMPUTE_PRENEX,
+ COMPUTE_VAR_ELIMINATION,
+ //COMPUTE_FLATTEN_ARGS_UF,
+ COMPUTE_CNF,
+ COMPUTE_LAST
+ };
+ static Node computeOperation( Node f, int computeOption );
+public:
+ static RewriteResponse preRewrite(TNode in);
+ static RewriteResponse postRewrite(TNode in);
+ static Node rewriteEquality(TNode equality) {
+ return postRewrite(equality).node;
+ }
+ static inline void init() {}
+ static inline void shutdown() {}
+private:
+ /** options */
+ static bool doMiniscopingNoFreeVar();
+ static bool doMiniscopingAnd();
+ static bool doOperation( Node f, bool isNested, int computeOption, bool duringRewrite = true );
+public:
+ static Node rewriteQuants( Node n, bool isNested = false, bool duringRewrite = true );
+ static Node rewriteQuant( Node n, bool isNested = false, bool duringRewrite = true );
+};/* class QuantifiersRewriter */
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
+
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
new file mode 100644
index 000000000..ead47e4b0
--- /dev/null
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -0,0 +1,199 @@
+/********************* */
+/*! \file theory_quantifiers.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 the theory of quantifiers
+ **
+ ** Implementation of the theory of quantifiers.
+ **/
+
+
+#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/valuation.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/instantiation_engine.h"
+#include "theory/quantifiers/model_engine.h"
+#include "expr/kind.h"
+#include "util/Assert.h"
+#include <map>
+#include <time.h>
+#include "theory/quantifiers/theory_quantifiers_instantiator.h"
+
+#define USE_FLIP_DECISION
+
+//static bool clockSet = false;
+//double initClock;
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
+ Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe),
+ d_numRestarts(0){
+ d_numInstantiations = 0;
+ d_baseDecLevel = -1;
+ if( Options::current()->finiteModelFind ){
+ qe->addModule( new ModelEngine( this ) );
+ }else{
+ qe->addModule( new InstantiationEngine( this ) );
+ }
+}
+
+
+TheoryQuantifiers::~TheoryQuantifiers() {
+}
+
+void TheoryQuantifiers::addSharedTerm(TNode t) {
+ Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): "
+ << t << endl;
+}
+
+
+void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
+ Debug("quantifiers-other") << "TheoryQuantifiers::notifyEq(): "
+ << lhs << " = " << rhs << endl;
+
+}
+
+void TheoryQuantifiers::preRegisterTerm(TNode n) {
+ Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
+ if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){
+ getQuantifiersEngine()->registerQuantifier( n );
+ }
+}
+
+
+void TheoryQuantifiers::presolve() {
+ Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl;
+}
+
+Node TheoryQuantifiers::getValue(TNode n) {
+ //NodeManager* nodeManager = NodeManager::currentNM();
+ switch(n.getKind()) {
+ case FORALL:
+ case EXISTS:
+ bool value;
+ if( d_valuation.hasSatValue( n, value ) ){
+ return NodeManager::currentNM()->mkConst(value);
+ }else{
+ return NodeManager::currentNM()->mkConst(false); //FIX_THIS?
+ }
+ break;
+ default:
+ Unhandled(n.getKind());
+ }
+}
+
+void TheoryQuantifiers::check(Effort e) {
+ CodeTimer codeTimer(d_theoryTime);
+
+ Debug("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
+ while(!done()) {
+ Node assertion = get();
+ Debug("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
+ switch(assertion.getKind()) {
+ case kind::FORALL:
+ assertUniversal( assertion );
+ break;
+ case kind::NOT:
+ {
+ switch( assertion[0].getKind()) {
+ case kind::FORALL:
+ assertExistential( assertion );
+ break;
+ default:
+ Unhandled(assertion[0].getKind());
+ break;
+ }
+ }
+ break;
+ default:
+ Unhandled(assertion.getKind());
+ break;
+ }
+ }
+ // call the quantifiers engine to check
+ getQuantifiersEngine()->check( e );
+}
+
+void TheoryQuantifiers::propagate(Effort level){
+ CodeTimer codeTimer(d_theoryTime);
+
+ getQuantifiersEngine()->propagate( level );
+}
+
+void TheoryQuantifiers::assertUniversal( Node n ){
+ Assert( n.getKind()==FORALL );
+ if( !n.hasAttribute(InstConstantAttribute()) ){
+ getQuantifiersEngine()->registerQuantifier( n );
+ getQuantifiersEngine()->assertNode( n );
+ }
+}
+
+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] );
+ NodeBuilder<> nb(kind::OR);
+ nb << n[0] << body.notNode();
+ Node lem = nb;
+ Debug("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
+ d_out->lemma( lem );
+ d_skolemized[n] = true;
+ }
+ }
+}
+
+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;
+ //}
+ //if( d_valuation.getDecisionLevel()>0 ){
+ // double r = double(rand())/double(RAND_MAX);
+ // unsigned decisionLevel = (unsigned)(r*d_valuation.getDecisionLevel());
+ // d_out->flipDecision( decisionLevel );
+ // return true;
+ //}else{
+ // return false;
+ //}
+
+ if( !d_out->flipDecision() ){
+ return restart();
+ }
+ return true;
+#endif
+}
+
+bool TheoryQuantifiers::restart(){
+ static const int restartLimit = 0;
+ if( d_numRestarts==restartLimit ){
+ Debug("quantifiers-flip") << "No more restarts." << std::endl;
+ return false;
+ }else{
+ d_numRestarts++;
+ Debug("quantifiers-flip") << "Do restart." << std::endl;
+ return true;
+ }
+}
+
+void TheoryQuantifiers::performCheck(Effort e){
+ getQuantifiersEngine()->check( e );
+}
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
new file mode 100644
index 000000000..05c3b9695
--- /dev/null
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -0,0 +1,77 @@
+/********************* */
+/*! \file theory_quantifiers.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 Theory of quantifiers.
+ **
+ ** Theory of quantifiers.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
+#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
+
+#include "theory/theory.h"
+#include "util/hash.h"
+#include "util/stats.h"
+
+#include <ext/hash_set>
+#include <iostream>
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TheoryEngine;
+
+class TheoryQuantifiers : public Theory {
+private:
+ typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
+ /** quantifiers that have been skolemized */
+ std::map< Node, bool > d_skolemized;
+ /** number of instantiations */
+ int d_numInstantiations;
+ int d_baseDecLevel;
+ /** number of restarts */
+ int d_numRestarts;
+
+ KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::quantifiers::theoryTime");
+
+public:
+ TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+ ~TheoryQuantifiers();
+
+ void addSharedTerm(TNode t);
+ void notifyEq(TNode lhs, TNode rhs);
+ void preRegisterTerm(TNode n);
+ void presolve();
+ void check(Effort e);
+ void propagate(Effort level);
+ Node getValue(TNode n);
+ void shutdown() { }
+ std::string identify() const { return std::string("TheoryQuantifiers"); }
+ bool flipDecision();
+private:
+ void assertUniversal( Node n );
+ void assertExistential( Node n );
+ bool restart();
+public:
+ void performCheck(Effort e);
+};/* class TheoryQuantifiers */
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
new file mode 100644
index 000000000..a5b6cc3bc
--- /dev/null
+++ b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
@@ -0,0 +1,76 @@
+/********************* */
+/*! \file theory_quantifiers_instantiator.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 theory_quantifiers_instantiator class
+ **/
+
+#include "theory/quantifiers/theory_quantifiers_instantiator.h"
+#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+InstantiatorTheoryQuantifiers::InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th) :
+Instantiator( c, ie, th ){
+
+}
+
+void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){
+ Debug("quant-quant-assert") << "InstantiatorTheoryQuantifiers::check: " << assertion << std::endl;
+ if( Options::current()->cbqi ){
+ if( assertion.hasAttribute(InstConstantAttribute()) ){
+ Debug("quant-quant-assert") << " -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl;
+ setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+ }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
+ Debug("quant-quant-assert") << " -> has constraints from " << assertion[0].getAttribute(InstConstantAttribute()) << std::endl;
+ setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+ }
+ }
+}
+
+void InstantiatorTheoryQuantifiers::processResetInstantiationRound( Theory::Effort effort ){
+
+}
+
+
+int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e, int limitInst ){
+ Debug("quant-quant") << "Quant: Try to solve (" << e << ") for " << f << "... " << std::endl;
+ if( e<5 ){
+ return InstStrategy::STATUS_UNFINISHED;
+ }else if( e==5 ){
+ //add random addition
+ if( isOwnerOf( f ) ){
+ InstMatch m;
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ ++(d_statistics.d_instantiations);
+ }
+ }
+ }
+ return InstStrategy::STATUS_UNKNOWN;
+}
+
+InstantiatorTheoryQuantifiers::Statistics::Statistics():
+ d_instantiations("InstantiatorTheoryQuantifiers::Instantiations_Total", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstantiatorTheoryQuantifiers::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h
new file mode 100644
index 000000000..dda3bfeaa
--- /dev/null
+++ b/src/theory/quantifiers/theory_quantifiers_instantiator.h
@@ -0,0 +1,60 @@
+/********************* */
+/*! \file instantiator_quantifiers_instantiator.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 instantiator_quantifiers_instantiator
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INSTANTIATOR_QUANTIFIERS_H
+#define __CVC4__INSTANTIATOR_QUANTIFIERS_H
+
+#include "theory/quantifiers_engine.h"
+
+#include "util/stats.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class InstantiatorTheoryQuantifiers : public Instantiator{
+ friend class QuantifiersEngine;
+public:
+ InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th);
+ ~InstantiatorTheoryQuantifiers() {}
+
+ /** check function, assertion is asserted to theory */
+ void assertNode( Node assertion );
+ /** identify */
+ std::string identify() const { return std::string("InstantiatorTheoryQuantifiers"); }
+private:
+ /** reset instantiation */
+ void processResetInstantiationRound( Theory::Effort effort );
+ /** process at effort */
+ int process( Node f, Theory::Effort effort, int e, int limitInst );
+
+ class Statistics {
+ public:
+ IntStat d_instantiations;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
+};/* class InstantiatiorTheoryArith */
+
+}
+}
+}
+
+#endif \ No newline at end of file
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
new file mode 100644
index 000000000..ceec36d7b
--- /dev/null
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -0,0 +1,113 @@
+/********************* */
+/*! \file theory_quantifiers_type_rules.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 Theory of quantifiers
+ **
+ ** Theory of quantifiers.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
+#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
+
+#include "util/matcher.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+struct QuantifierForallTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw(TypeCheckingExceptionPrivate) {
+ Debug("typecheck-q") << "type check for fa " << n << std::endl;
+ Assert(n.getKind() == kind::FORALL && n.getNumChildren()>0 );
+ if( check ){
+ if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
+ throw TypeCheckingExceptionPrivate(n, "first argument of universal quantifier is not bound var list");
+ }
+ if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
+ throw TypeCheckingExceptionPrivate(n, "body of universal quantifier is not boolean");
+ }
+ if( n.getNumChildren()==3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
+ throw TypeCheckingExceptionPrivate(n, "third argument of universal quantifier is not instantiation pattern list");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* struct QuantifierForallTypeRule */
+
+struct QuantifierExistsTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw(TypeCheckingExceptionPrivate) {
+ Debug("typecheck-q") << "type check for ex " << n << std::endl;
+ Assert(n.getKind() == kind::EXISTS && n.getNumChildren()>0 );
+ if( check ){
+ if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
+ throw TypeCheckingExceptionPrivate(n, "first argument of existential quantifier is not bound var list");
+ }
+ if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
+ throw TypeCheckingExceptionPrivate(n, "body of existential quantifier is not boolean");
+ }
+ if( n.getNumChildren()==3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
+ throw TypeCheckingExceptionPrivate(n, "third argument of existential quantifier is not instantiation pattern list");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* struct QuantifierExistsTypeRule */
+
+struct QuantifierBoundVarListTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw(TypeCheckingExceptionPrivate) {
+ Assert(n.getKind() == kind::BOUND_VAR_LIST );
+ if( check ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( n[i].getKind()!=kind::VARIABLE ){
+ throw TypeCheckingExceptionPrivate(n, "argument of bound var list is not variable");
+ }
+ }
+ }
+ return nodeManager->boundVarListType();
+ }
+};/* struct QuantifierBoundVarListTypeRule */
+
+struct QuantifierInstPatternTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw(TypeCheckingExceptionPrivate) {
+ Assert(n.getKind() == kind::INST_PATTERN );
+ return nodeManager->instPatternType();
+ }
+};/* struct QuantifierInstPatternTypeRule */
+
+
+struct QuantifierInstPatternListTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw(TypeCheckingExceptionPrivate) {
+ Assert(n.getKind() == kind::INST_PATTERN_LIST );
+ if( check ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( n[i].getKind()!=kind::INST_PATTERN ){
+ throw TypeCheckingExceptionPrivate(n, "argument of inst pattern list is not inst pattern");
+ }
+ }
+ }
+ return nodeManager->instPatternListType();
+ }
+};/* struct QuantifierInstPatternListTypeRule */
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback