diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/Makefile | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/Makefile.am | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 393 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 79 | ||||
-rw-r--r-- | src/theory/quantifiers/kinds | 48 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 1401 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 369 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 722 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 88 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 199 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 77 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_instantiator.cpp | 76 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_instantiator.h | 60 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_type_rules.h | 113 |
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 */ |