diff options
Diffstat (limited to 'src/theory/quantifiers')
41 files changed, 4517 insertions, 964 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 7fea8cf3a..be24d6c67 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -23,8 +23,6 @@ libquantifiers_la_SOURCES = \ model_engine.cpp \ modes.cpp \ modes.h \ - relevant_domain.h \ - relevant_domain.cpp \ term_database.h \ term_database.cpp \ first_order_model.h \ @@ -44,7 +42,20 @@ libquantifiers_la_SOURCES = \ inst_strategy_e_matching.h \ inst_strategy_e_matching.cpp \ inst_strategy_cbqi.h \ - inst_strategy_cbqi.cpp + inst_strategy_cbqi.cpp \ + full_model_check.h \ + full_model_check.cpp \ + bounded_integers.h \ + bounded_integers.cpp \ + first_order_reasoning.h \ + first_order_reasoning.cpp \ + rewrite_engine.h \ + rewrite_engine.cpp \ + relevant_domain.h \ + relevant_domain.cpp \ + symmetry_breaking.h \ + symmetry_breaking.cpp + EXTRA_DIST = \ kinds \ diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp new file mode 100644 index 000000000..30ff5242b --- /dev/null +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -0,0 +1,372 @@ +/********************* */ +/*! \file bounded_integers.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bounded integers module + ** + ** This class manages integer bounds for quantifiers + **/ + +#include "theory/quantifiers/bounded_integers.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/model_engine.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +void BoundedIntegers::RangeModel::initialize() { + //add initial split lemma + Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) ); + ltr = Rewriter::rewrite( ltr ); + Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr << std::endl; + d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr ); + Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr; + d_range_literal[-1] = ltr_lit; + d_lit_to_range[ltr_lit] = -1; + d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT; + //register with bounded integers + Trace("bound-int-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl; + d_bi->addLiteralFromRange(ltr_lit, d_range); +} + +void BoundedIntegers::RangeModel::assertNode(Node n) { + bool pol = n.getKind()!=NOT; + Node nlit = n.getKind()==NOT ? n[0] : n; + if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){ + Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")"; + Trace("bound-int-assert") << ", found literal " << nlit; + Trace("bound-int-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl; + d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]); + if( pol!=d_lit_to_pol[nlit] ){ + //check if we need a new split? + if( !d_has_range ){ + bool needsRange = true; + for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ + if( d_range_assertions.find( it->first )==d_range_assertions.end() ){ + needsRange = false; + break; + } + } + if( needsRange ){ + allocateRange(); + } + } + }else{ + if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){ + Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl; + d_curr_range = d_lit_to_range[nlit]; + } + //set the range + d_has_range = true; + } + }else{ + Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl; + exit(0); + } +} + +void BoundedIntegers::RangeModel::allocateRange() { + d_curr_max++; + int newBound = d_curr_max; + Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl; + //TODO: newBound should be chosen in a smarter way + Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) ); + ltr = Rewriter::rewrite( ltr ); + Trace("bound-int-lemma") << " *** bound int: split on " << ltr << std::endl; + d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr ); + Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr; + d_range_literal[newBound] = ltr_lit; + d_lit_to_range[ltr_lit] = newBound; + d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT; + //register with bounded integers + d_bi->addLiteralFromRange(ltr_lit, d_range); +} + +Node BoundedIntegers::RangeModel::getNextDecisionRequest() { + //request the current cardinality as a decision literal, if not already asserted + for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ + int i = it->second; + if( !d_has_range || i<d_curr_range ){ + Node rn = it->first; + Assert( !rn.isNull() ); + if( d_range_assertions.find( rn )==d_range_assertions.end() ){ + if (!d_lit_to_pol[it->first]) { + rn = rn.negate(); + } + Trace("bound-int-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl; + return rn; + } + } + } + return Node::null(); +} + + +BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) : +QuantifiersModule(qe), d_assertions(c){ + +} + +bool BoundedIntegers::isBound( Node f, Node v ) { + return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); +} + +bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) { + if( b.getKind()==BOUND_VARIABLE ){ + if( !isBound( f, b ) ){ + return true; + } + }else{ + for( unsigned i=0; i<b.getNumChildren(); i++ ){ + if( hasNonBoundVar( f, b[i] ) ){ + return true; + } + } + } + return false; +} + +void BoundedIntegers::processLiteral( Node f, Node lit, bool pol, + std::map< int, std::map< Node, Node > >& bound_lit_map, + std::map< int, std::map< Node, bool > >& bound_lit_pol_map ) { + if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){ + std::map< Node, Node > msum; + if (QuantArith::getMonomialSumLit( lit, msum )){ + Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl; + for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + Trace("bound-int-debug") << " "; + if( !it->second.isNull() ){ + Trace("bound-int-debug") << it->second; + if( !it->first.isNull() ){ + Trace("bound-int-debug") << " * "; + } + } + if( !it->first.isNull() ){ + Trace("bound-int-debug") << it->first; + } + Trace("bound-int-debug") << std::endl; + } + Trace("bound-int-debug") << std::endl; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){ + Node veq; + if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){ + Node n1 = veq[0]; + Node n2 = veq[1]; + if(pol){ + //flip + n1 = veq[1]; + n2 = veq[0]; + if( n1.getKind()==BOUND_VARIABLE ){ + n2 = QuantArith::offset( n2, 1 ); + }else{ + n1 = QuantArith::offset( n1, -1 ); + } + veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 ); + } + Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl; + Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2; + if( !isBound( f, bv ) ){ + if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) { + Trace("bound-int-debug") << "The bound is relevant." << std::endl; + int loru = n1.getKind()==BOUND_VARIABLE ? 0 : 1; + d_bounds[loru][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1); + bound_lit_map[loru][bv] = lit; + bound_lit_pol_map[loru][bv] = pol; + } + } + } + } + } + } + }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) { + Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; + exit(0); + } +} + +void BoundedIntegers::process( Node f, Node n, bool pol, + std::map< int, std::map< Node, Node > >& bound_lit_map, + std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){ + if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){ + for( unsigned i=0; i<n.getNumChildren(); i++) { + bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol; + process( f, n[i], newPol, bound_lit_map, bound_lit_pol_map ); + } + }else if( n.getKind()==NOT ){ + process( f, n[0], !pol, bound_lit_map, bound_lit_pol_map ); + }else { + processLiteral( f, n, pol, bound_lit_map, bound_lit_pol_map ); + } +} + +void BoundedIntegers::check( Theory::Effort e ) { + +} + + +void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) { + d_lit_to_ranges[lit].push_back(r); + //check if it is already asserted? + if(d_assertions.find(lit)!=d_assertions.end()){ + d_rms[r]->assertNode( d_assertions[lit] ? lit : lit.negate() ); + } +} + +void BoundedIntegers::registerQuantifier( Node f ) { + Trace("bound-int") << "Register quantifier " << f << std::endl; + bool hasIntType = false; + int finiteTypes = 0; + std::map< Node, int > numMap; + for( unsigned i=0; i<f[0].getNumChildren(); i++) { + numMap[f[0][i]] = i; + if( f[0][i].getType().isInteger() ){ + hasIntType = true; + } + else if( f[0][i].getType().isSort() ){ + finiteTypes++; + } + } + if( hasIntType ){ + bool success; + do{ + std::map< int, std::map< Node, Node > > bound_lit_map; + std::map< int, std::map< Node, bool > > bound_lit_pol_map; + success = false; + process( f, f[1], true, bound_lit_map, bound_lit_pol_map ); + for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){ + Node v = it->first; + if( !isBound(f,v) ){ + if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){ + d_set[f].push_back(v); + d_set_nums[f].push_back(numMap[v]); + success = true; + //set Attributes on literals + for( unsigned b=0; b<2; b++ ){ + Assert( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ); + Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() ); + BoundIntLitAttribute bila; + bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 ); + } + Trace("bound-int") << "Variable " << v << " is bound because of literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl; + } + } + } + }while( success ); + Trace("bound-int") << "Bounds are : " << std::endl; + for( unsigned i=0; i<d_set[f].size(); i++) { + Node v = d_set[f][i]; + Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] ); + d_range[f][v] = Rewriter::rewrite( r ); + Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl; + } + if( d_set[f].size()==(f[0].getNumChildren()-finiteTypes) ){ + d_bound_quants.push_back( f ); + for( unsigned i=0; i<d_set[f].size(); i++) { + Node v = d_set[f][i]; + Node r = d_range[f][v]; + if( quantifiers::TermDb::hasBoundVarAttr(r) ){ + //introduce a new bound + Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" ); + d_nground_range[f][v] = d_range[f][v]; + d_range[f][v] = new_range; + r = new_range; + } + if( r.getKind()!=CONST_RATIONAL ){ + if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){ + Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl; + d_ranges.push_back( r ); + d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() ); + d_rms[r]->initialize(); + } + } + } + }else{ + Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl; + } + } +} + +void BoundedIntegers::assertNode( Node n ) { + Trace("bound-int-assert") << "Assert " << n << std::endl; + Node nlit = n.getKind()==NOT ? n[0] : n; + if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){ + Trace("bound-int-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl; + for( unsigned i=0; i<d_lit_to_ranges[nlit].size(); i++) { + Node r = d_lit_to_ranges[nlit][i]; + Trace("bound-int-assert") << " ...this is a bounding literal for " << r << std::endl; + d_rms[r]->assertNode( n ); + } + } + d_assertions[nlit] = n.getKind()!=NOT; +} + +Node BoundedIntegers::getNextDecisionRequest() { + Trace("bound-int-dec") << "bi: Get next decision request?" << std::endl; + for( unsigned i=0; i<d_ranges.size(); i++) { + Node d = d_rms[d_ranges[i]]->getNextDecisionRequest(); + if (!d.isNull()) { + return d; + } + } + return Node::null(); +} + +void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { + l = d_bounds[0][f][v]; + u = d_bounds[1][f][v]; + if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){ + //must create substitution + std::vector< Node > vars; + std::vector< Node > subs; + Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl; + for( unsigned i=0; i<d_set[f].size(); i++) { + if( d_set[f][i]!=v ){ + Trace("bound-int-rsi") << "Look up the value for " << d_set[f][i] << " " << rsi->d_var_order[d_set_nums[f][i]] << std::endl; + Trace("bound-int-rsi") << "term : " << rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]) << std::endl; + vars.push_back(d_set[f][i]); + subs.push_back(rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]])); + }else{ + break; + } + } + Trace("bound-int-rsi") << "Do substitution..." << std::endl; + //check if it has been instantiated + if (!vars.empty() && !d_bnd_it[f][v].hasInstantiated(subs)){ + //must add the lemma + Node nn = d_nground_range[f][v]; + nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] ); + Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma(lem); + l = Node::null(); + u = Node::null(); + return; + }else{ + u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + } + } +} + +void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { + getBounds( f, v, rsi, l, u ); + Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl; + l = d_quantEngine->getModel()->getCurrentModelValue( l ); + u = d_quantEngine->getModel()->getCurrentModelValue( u ); + Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl; + return; +} + +bool BoundedIntegers::isGroundRange(Node f, Node v) { + return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v)); +} diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h new file mode 100644 index 000000000..3da938d31 --- /dev/null +++ b/src/theory/quantifiers/bounded_integers.h @@ -0,0 +1,127 @@ +/********************* */ +/*! \file bounded_integers.h +** \verbatim +** Original author: Andrew Reynolds +** This file is part of the CVC4 project. +** Copyright (c) 2009-2013 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief This class manages integer bounds for quantifiers +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BOUNDED_INTEGERS_H +#define __CVC4__BOUNDED_INTEGERS_H + + +#include "theory/quantifiers_engine.h" + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.h" + +namespace CVC4 { +namespace theory { + +class RepSetIterator; + +namespace quantifiers { + + +class BoundedIntegers : public QuantifiersModule +{ + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; +private: + //for determining bounds + bool isBound( Node f, Node v ); + bool hasNonBoundVar( Node f, Node b ); + std::map< Node, std::map< Node, Node > > d_bounds[2]; + std::map< Node, std::vector< Node > > d_set; + std::map< Node, std::vector< int > > d_set_nums; + std::map< Node, std::map< Node, Node > > d_range; + std::map< Node, std::map< Node, Node > > d_nground_range; + void hasFreeVar( Node f, Node n ); + void process( Node f, Node n, bool pol, + std::map< int, std::map< Node, Node > >& bound_lit_map, + std::map< int, std::map< Node, bool > >& bound_lit_pol_map ); + void processLiteral( Node f, Node lit, bool pol, + std::map< int, std::map< Node, Node > >& bound_lit_map, + std::map< int, std::map< Node, bool > >& bound_lit_pol_map ); + std::vector< Node > d_bound_quants; +private: + class RangeModel { + private: + BoundedIntegers * d_bi; + void allocateRange(); + public: + RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi), + d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {} + Node d_range; + int d_curr_max; + std::map< int, Node > d_range_literal; + std::map< Node, bool > d_lit_to_pol; + std::map< Node, int > d_lit_to_range; + NodeBoolMap d_range_assertions; + context::CDO< bool > d_has_range; + context::CDO< int > d_curr_range; + void initialize(); + void assertNode(Node n); + Node getNextDecisionRequest(); + }; +private: + //information for minimizing ranges + std::vector< Node > d_ranges; + //map to range model objects + std::map< Node, RangeModel * > d_rms; + //literal to range + std::map< Node, std::vector< Node > > d_lit_to_ranges; + //list of currently asserted arithmetic literals + NodeBoolMap d_assertions; +private: + //class to store whether bounding lemmas have been added + class BoundInstTrie + { + public: + std::map< Node, BoundInstTrie > d_children; + bool hasInstantiated( std::vector< Node > & vals, int index = 0, bool madeNew = false ){ + if( index>=(int)vals.size() ){ + return !madeNew; + }else{ + Node n = vals[index]; + if( d_children.find(n)==d_children.end() ){ + madeNew = true; + } + return d_children[n].hasInstantiated(vals,index+1,madeNew); + } + } + }; + std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; +private: + void addLiteralFromRange( Node lit, Node r ); +public: + BoundedIntegers( context::Context* c, QuantifiersEngine* qe ); + + void check( Theory::Effort e ); + void registerQuantifier( Node f ); + void assertNode( Node n ); + Node getNextDecisionRequest(); + bool isBoundVar( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); } + unsigned getNumBoundVars( Node f ) { return d_set[f].size(); } + Node getBoundVar( Node f, int i ) { return d_set[f][i]; } + int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; } + Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; } + Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; } + void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); + void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); + bool isGroundRange(Node f, Node v); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 0c423de19..42b49cf01 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -27,7 +27,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; bool CandidateGenerator::isLegalCandidate( Node n ){ - return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute()) ) ); + return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ) ); } void CandidateGeneratorQueue::addCandidate( Node n ) { @@ -149,7 +149,7 @@ void CandidateGeneratorQELitEq::reset( Node eqc ){ d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); } Node CandidateGeneratorQELitEq::getNextCandidate(){ - while( d_eq.isFinished() ){ + while( !d_eq.isFinished() ){ Node n = (*d_eq); ++d_eq; if( n.getType()==d_match_pattern[0].getType() ){ @@ -186,3 +186,29 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){ } return Node::null(); } + + +CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : + d_match_pattern( mpat ), d_qe( qe ){ + +} + +void CandidateGeneratorQEAll::resetInstantiationRound() { + +} + +void CandidateGeneratorQEAll::reset( Node eqc ) { + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); +} + +Node CandidateGeneratorQEAll::getNextCandidate() { + while( !d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType()==d_match_pattern.getType() ){ + //an equivalence class with the same type as the pattern, return it + return n; + } + } + return Node::null(); +} diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 81b98ce0a..402a29848 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -69,8 +69,7 @@ public: Node getNextCandidate(); };/* class CandidateGeneratorQueue */ -class CandidateGeneratorQEDisequal; - +//the default generator class CandidateGeneratorQE : public CandidateGenerator { friend class CandidateGeneratorQEDisequal; @@ -93,27 +92,6 @@ public: Node getNextCandidate(); }; - -//class CandidateGeneratorQEDisequal : public CandidateGenerator -//{ -//private: -// //equivalence class -// Node d_eq_class; -// //equivalence class info -// EqClassInfo* d_eci; -// //equivalence class iterator -// EqClassInfo::BoolMap::const_iterator d_eqci_iter; -// //instantiator pointer -// QuantifiersEngine* d_qe; -//public: -// CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ); -// ~CandidateGeneratorQEDisequal(){} -// -// void resetInstantiationRound(); -// void reset( Node eqc ); //should be what you want to be disequal from -// Node getNextCandidate(); -//}; - class CandidateGeneratorQELitEq : public CandidateGenerator { private: @@ -150,6 +128,24 @@ public: Node getNextCandidate(); }; +class CandidateGeneratorQEAll : public CandidateGenerator +{ +private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + //einstantiator pointer + QuantifiersEngine* d_qe; +public: + CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); + ~CandidateGeneratorQEAll(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index bba9c0163..63cac9c15 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -25,6 +25,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; +using namespace CVC4::theory::quantifiers::fmcheck; FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ @@ -38,15 +39,34 @@ void FirstOrderModel::assertQuantifier( Node n ){ } } -void FirstOrderModel::reset(){ - TheoryModel::reset(); +Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) { + std::vector< Node > children; + if( n.getNumChildren()>0 ){ + if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for (unsigned i=0; i<n.getNumChildren(); i++) { + Node nc = getCurrentModelValue( n[i], partial ); + if (nc.isNull()) { + return Node::null(); + }else{ + children.push_back( nc ); + } + } + if( n.getKind()==APPLY_UF ){ + return getCurrentUfModelValue( n, children, partial ); + }else{ + Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); + nn = Rewriter::rewrite( nn ); + return nn; + } + }else{ + return getRepresentative(n); + } } -void FirstOrderModel::initialize( bool considerAxioms ){ - //rebuild models - d_uf_model_tree.clear(); - d_uf_model_gen.clear(); - d_array_model.clear(); +void FirstOrderModel::initialize( bool considerAxioms ) { + processInitialize(); //this is called after representatives have been chosen and the equality engine has been built //for each quantifier, collect all operators we care about for( int i=0; i<getNumAssertedQuantifiers(); i++ ){ @@ -59,6 +79,23 @@ void FirstOrderModel::initialize( bool considerAxioms ){ } void FirstOrderModel::initializeModelForTerm( Node n ){ + processInitializeModelForTerm( n ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + initializeModelForTerm( n[i] ); + } +} + +FirstOrderModelIG::FirstOrderModelIG(context::Context* c, std::string name) : FirstOrderModel(c,name) { + +} + +void FirstOrderModelIG::processInitialize(){ + //rebuild models + d_uf_model_tree.clear(); + d_uf_model_gen.clear(); +} + +void FirstOrderModelIG::processInitializeModelForTerm( Node n ){ if( n.getKind()==APPLY_UF ){ Node op = n.getOperator(); if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ @@ -82,14 +119,11 @@ void FirstOrderModel::initializeModelForTerm( Node n ){ } } */ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - initializeModelForTerm( n[i] ); - } } //for evaluation of quantifier bodies -void FirstOrderModel::resetEvaluate(){ +void FirstOrderModelIG::resetEvaluate(){ d_eval_uf_use_default.clear(); d_eval_uf_model.clear(); d_eval_term_index_order.clear(); @@ -107,7 +141,7 @@ void FirstOrderModel::resetEvaluate(){ // if eVal = 0, then n' cannot be proven to be equal to phaseReq // if eVal is not 0, then // each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model -int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ +int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ ++d_eval_formulas; //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl; //Notice() << "Eval " << n << std::endl; @@ -226,7 +260,7 @@ int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ } } -Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ +Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ //Message() << "Eval term " << n << std::endl; Node val; depIndex = ri->getNumTerms()-1; @@ -342,7 +376,7 @@ Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ return val; } -Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){ +Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){ depIndex = -1; if( n.getNumChildren()==0 ){ return n; @@ -372,14 +406,14 @@ Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< i } } -void FirstOrderModel::clearEvalFailed( int index ){ +void FirstOrderModelIG::clearEvalFailed( int index ){ for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){ d_eval_failed[ d_eval_failed_lits[index][i] ] = false; } d_eval_failed_lits[index].clear(); } -void FirstOrderModel::makeEvalUfModel( Node n ){ +void FirstOrderModelIG::makeEvalUfModel( Node n ){ if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){ makeEvalUfIndexOrder( n ); if( !d_eval_uf_use_default[n] ){ @@ -397,7 +431,7 @@ struct sortGetMaxVariableNum { int computeMaxVariableNum( Node n ){ if( n.getKind()==INST_CONSTANT ){ return n.getAttribute(InstVarNumAttribute()); - }else if( n.hasAttribute(InstConstantAttribute()) ){ + }else if( TermDb::hasInstConstAttr(n) ){ int maxVal = -1; for( int i=0; i<(int)n.getNumChildren(); i++ ){ int val = getMaxVariableNum( n[i] ); @@ -423,7 +457,7 @@ struct sortGetMaxVariableNum { bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));} }; -void FirstOrderModel::makeEvalUfIndexOrder( Node n ){ +void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){ if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ #ifdef USE_INDEX_ORDERING //sort arguments in order of least significant vs. most significant variable in default ordering @@ -460,3 +494,187 @@ void FirstOrderModel::makeEvalUfIndexOrder( Node n ){ #endif } } + +Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { + std::vector< Node > children; + children.push_back(n.getOperator()); + children.insert(children.end(), args.begin(), args.end()); + Node nv = NodeManager::currentNM()->mkNode(APPLY_UF, children); + //make the term model specifically for nv + makeEvalUfModel( nv ); + int argDepIndex; + if( d_eval_uf_use_default[nv] ){ + return d_uf_model_tree[ n.getOperator() ].getValue( this, nv, argDepIndex ); + }else{ + return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex ); + } +} + + + + + + +FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : +FirstOrderModel(c, name), d_qe(qe){ + +} + +Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { + //Assert( fm->hasTerm(n) ); + TypeNode tn = n.getType(); + if( tn.isBoolean() ){ + return areEqual(n, d_true) ? d_true : d_false; + }else{ + if( !hasTerm(n) ){ + if( strict ){ + return Node::null(); + }else{ + Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl; + } + } + Node r = getRepresentative(n); + if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){ + if (r==d_model_basis_rep[tn]) { + r = d_qe->getTermDatabase()->getModelBasisTerm(tn); + } + } + return r; + } +} + +Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { + Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl; + for(unsigned i=0; i<args.size(); i++) { + args[i] = getUsedRepresentative(args[i]); + } + Assert( n.getKind()==APPLY_UF ); + return d_models[n.getOperator()]->evaluate(this, args); +} + +void FirstOrderModelFmc::processInitialize() { + if( options::fmfFmcInterval() && intervalOp.isNull() ){ + std::vector< TypeNode > types; + for(unsigned i=0; i<2; i++){ + types.push_back(NodeManager::currentNM()->integerType()); + } + TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() ); + intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" ); + } + for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){ + it->second->reset(); + } + d_model_basis_rep.clear(); +} + +void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { + if( n.getKind()==APPLY_UF ){ + if( d_models.find(n.getOperator())==d_models.end()) { + d_models[n.getOperator()] = new Def; + } + } +} + +Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){ + //check if there is even any domain elements at all + if (!d_rep_set.hasType(tn)) { + Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); + d_rep_set.d_type_reps[tn].push_back(mbt); + }else if( d_rep_set.d_type_reps[tn].size()==0 ){ + Message() << "empty reps" << std::endl; + exit(0); + } + return d_rep_set.d_type_reps[tn][0]; +} + + +bool FirstOrderModelFmc::isStar(Node n) { + return n==getStar(n.getType()); +} + +Node FirstOrderModelFmc::getStar(TypeNode tn) { + if( d_type_star.find(tn)==d_type_star.end() ){ + Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" ); + d_type_star[tn] = st; + } + return d_type_star[tn]; +} + +Node FirstOrderModelFmc::getStarElement(TypeNode tn) { + Node st = getStar(tn); + if( options::fmfFmcInterval() && tn.isInteger() ){ + st = getInterval( st, st ); + } + return st; +} + +bool FirstOrderModelFmc::isModelBasisTerm(Node n) { + return n==getModelBasisTerm(n.getType()); +} + +Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) { + return d_qe->getTermDatabase()->getModelBasisTerm(tn); +} + +Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { + Trace("fmc-model") << "Get function value for " << op << std::endl; + TypeNode type = op.getType(); + std::vector< Node > vars; + for( size_t i=0; i<type.getNumChildren()-1; i++ ){ + std::stringstream ss; + ss << argPrefix << (i+1); + Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ); + vars.push_back( b ); + } + Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); + Node curr; + for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { + Node v = getRepresentative( d_models[op]->d_value[i] ); + if( curr.isNull() ){ + curr = v; + }else{ + //make the condition + Node cond = d_models[op]->d_cond[i]; + std::vector< Node > children; + for( unsigned j=0; j<cond.getNumChildren(); j++) { + if (isInterval(cond[j])){ + if( !isStar(cond[j][0]) ){ + children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) ); + } + if( !isStar(cond[j][1]) ){ + children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) ); + } + }else if (!isStar(cond[j])){ + Node c = getUsedRepresentative( cond[j] ); + children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); + } + } + Assert( !children.empty() ); + Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); + curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); + } + } + curr = Rewriter::rewrite( curr ); + return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); +} + +bool FirstOrderModelFmc::isInterval(Node n) { + return n.getKind()==APPLY_UF && n.getOperator()==intervalOp; +} + +Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){ + return NodeManager::currentNM()->mkNode( APPLY_UF, intervalOp, lb, ub ); +} + +bool FirstOrderModelFmc::isInRange( Node v, Node i ) { + for( unsigned b=0; b<2; b++ ){ + if( !isStar( i[b] ) ){ + if( ( b==0 && i[b].getConst<Rational>() > v.getConst<Rational>() ) || + ( b==1 && i[b].getConst<Rational>() <= v.getConst<Rational>() ) ){ + return false; + } + } + } + return true; +} diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 76f21e19c..f6e012660 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -19,7 +19,6 @@ #include "theory/model.h" #include "theory/uf/theory_uf_model.h" -#include "theory/arrays/theory_arrays_model.h" namespace CVC4 { namespace theory { @@ -30,33 +29,22 @@ namespace quantifiers{ class TermDb; +class FirstOrderModelIG; +namespace fmcheck { + class FirstOrderModelFmc; +} + class FirstOrderModel : public TheoryModel { private: - //for initialize model - void initializeModelForTerm( Node n ); /** whether an axiom is asserted */ context::CDO< bool > d_axiom_asserted; /** list of quantifiers asserted in the current context */ context::CDList<Node> d_forall_asserts; /** is model set */ context::CDO< bool > d_isModelSet; -public: //for Theory UF: - //models for each UF operator - std::map< Node, uf::UfModelTree > d_uf_model_tree; - //model generators - std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen; -private: - //map from terms to the models used to calculate their value - std::map< Node, bool > d_eval_uf_use_default; - std::map< Node, uf::UfModelTree > d_eval_uf_model; - void makeEvalUfModel( Node n ); - //index ordering to use for each term - std::map< Node, std::vector< int > > d_eval_term_index_order; - void makeEvalUfIndexOrder( Node n ); -public: //for Theory Arrays: - //default value for each non-store array - std::map< Node, arrays::ArrayModel > d_array_model; + /** get current model value */ + virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0; public: //for Theory Quantifiers: /** assert quantifier */ void assertQuantifier( Node n ); @@ -66,19 +54,51 @@ public: //for Theory Quantifiers: Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } /** bool axiom asserted */ bool isAxiomAsserted() { return d_axiom_asserted; } + /** initialize model for term */ + void initializeModelForTerm( Node n ); + virtual void processInitializeModelForTerm( Node n ) = 0; public: FirstOrderModel( context::Context* c, std::string name ); virtual ~FirstOrderModel(){} - // reset the model - void reset(); + virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; } + virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; } // initialize the model void initialize( bool considerAxioms = true ); + virtual void processInitialize() = 0; /** mark model set */ void markModelSet() { d_isModelSet = true; } /** is model set */ bool isModelSet() { return d_isModelSet; } + /** get current model value */ + Node getCurrentModelValue( Node n, bool partial = false ); +};/* class FirstOrderModel */ + + +class FirstOrderModelIG : public FirstOrderModel +{ +public: //for Theory UF: + //models for each UF operator + std::map< Node, uf::UfModelTree > d_uf_model_tree; + //model generators + std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen; +private: + //map from terms to the models used to calculate their value + std::map< Node, bool > d_eval_uf_use_default; + std::map< Node, uf::UfModelTree > d_eval_uf_model; + void makeEvalUfModel( Node n ); + //index ordering to use for each term + std::map< Node, std::vector< int > > d_eval_term_index_order; + void makeEvalUfIndexOrder( Node n ); + /** get current model value */ + Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); //the following functions are for evaluating quantifier bodies public: + FirstOrderModelIG(context::Context* c, std::string name); + FirstOrderModelIG * asFirstOrderModelIG() { return this; } + // initialize the model + void processInitialize(); + //for initialize model + void processInitializeModelForTerm( Node n ); /** reset evaluation */ void resetEvaluate(); /** evaluate functions */ @@ -97,7 +117,49 @@ private: void clearEvalFailed( int index ); std::map< Node, bool > d_eval_failed; std::map< int, std::vector< Node > > d_eval_failed_lits; -};/* class FirstOrderModel */ +}; + + +namespace fmcheck { + +class Def; + +class FirstOrderModelFmc : public FirstOrderModel +{ + friend class FullModelChecker; +private: + /** quant engine */ + QuantifiersEngine * d_qe; + /** models for UF */ + std::map<Node, Def * > d_models; + std::map<TypeNode, Node > d_model_basis_rep; + std::map<TypeNode, Node > d_type_star; + Node intervalOp; + Node getUsedRepresentative(Node n, bool strict = false); + /** get current model value */ + Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); + void processInitializeModelForTerm(Node n); +public: + FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); + FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } + // initialize the model + void processInitialize(); + + Node getFunctionValue(Node op, const char* argPrefix ); + + bool isStar(Node n); + Node getStar(TypeNode tn); + Node getStarElement(TypeNode tn); + bool isModelBasisTerm(Node n); + Node getModelBasisTerm(TypeNode tn); + Node getSomeDomainElement(TypeNode tn); + bool isInterval(Node n); + Node getInterval( Node lb, Node ub ); + bool isInRange( Node v, Node i ); +}; + +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp new file mode 100644 index 000000000..ebfb55f08 --- /dev/null +++ b/src/theory/quantifiers/first_order_reasoning.cpp @@ -0,0 +1,171 @@ +/********************* */ +/*! \file first_order_reasoning.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-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief first order reasoning module + ** + **/ + +#include <vector> + +#include "theory/quantifiers/first_order_reasoning.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { + + +void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){ + if( n.getKind()==FORALL ){ + collectLits( n[1], lits ); + }else if( n.getKind()==OR ){ + for(unsigned j=0; j<n.getNumChildren(); j++) { + collectLits(n[j], lits ); + } + }else{ + lits.push_back( n ); + } +} + +void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){ + for( unsigned i=0; i<assertions.size(); i++) { + Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl; + } + + //process all assertions + int num_processed; + int num_true = 0; + int num_rounds = 0; + do { + num_processed = 0; + for( unsigned i=0; i<assertions.size(); i++ ){ + if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){ + std::vector< Node > fo_lits; + collectLits( assertions[i], fo_lits ); + Node unitLit = process( assertions[i], fo_lits ); + if( !unitLit.isNull() ){ + Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl; + bool pol = unitLit.getKind()!=NOT; + unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit; + if( unitLit.getKind()==EQUAL ){ + + }else if( unitLit.getKind()==APPLY_UF ){ + //make sure all are unique vars; + bool success = true; + std::vector< Node > unique_vars; + for( unsigned j=0; j<unitLit.getNumChildren(); j++) { + if( unitLit[j].getKind()==BOUND_VARIABLE ){ + if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){ + unique_vars.push_back( unitLit[j] ); + }else{ + success = false; + break; + } + }else{ + success = false; + break; + } + } + if( success ){ + d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol); + Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl; + Trace("fo-rsn") << " from : " << assertions[i] << std::endl; + d_assertion_true[assertions[i]] = true; + num_processed++; + } + }else if( unitLit.getKind()==VARIABLE ){ + d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol); + Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl; + Trace("fo-rsn") << " from : " << assertions[i] << std::endl; + d_assertion_true[assertions[i]] = true; + num_processed++; + } + } + if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){ + num_true++; + } + } + } + num_rounds++; + }while( num_processed>0 ); + Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl; + for( unsigned i=0; i<assertions.size(); i++ ){ + assertions[i] = theory::Rewriter::rewrite( simplify( assertions[i] ) ); + } +} + +Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) { + int index = -1; + for( unsigned i=0; i<lits.size(); i++) { + bool pol = lits[i].getKind()!=NOT; + Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i]; + Node litDef; + if( n.getKind()==APPLY_UF ){ + if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ + litDef = d_const_def[n.getOperator()]; + } + }else if( n.getKind()==VARIABLE ){ + if( d_const_def.find(n)!=d_const_def.end() ){ + litDef = d_const_def[n]; + } + } + if( !litDef.isNull() ){ + Node poln = NodeManager::currentNM()->mkConst( pol ); + if( litDef==poln ){ + Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl; + d_assertion_true[a] = true; + return Node::null(); + } + } + if( litDef.isNull() ){ + if( index==-1 ){ + //store undefined index + index = i; + }else{ + //two undefined, return null + return Node::null(); + } + } + } + if( index!=-1 ){ + return lits[index]; + }else{ + return Node::null(); + } +} + +Node FirstOrderPropagation::simplify( Node n ) { + if( n.getKind()==VARIABLE ){ + if( d_const_def.find(n)!=d_const_def.end() ){ + return d_const_def[n]; + } + }else if( n.getKind()==APPLY_UF ){ + if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ + return d_const_def[n.getOperator()]; + } + } + if( n.getNumChildren()==0 ){ + return n; + }else{ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for(unsigned i=0; i<n.getNumChildren(); i++) { + children.push_back( simplify(n[i]) ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + } +} + +} diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h new file mode 100644 index 000000000..5f217050c --- /dev/null +++ b/src/theory/quantifiers/first_order_reasoning.h @@ -0,0 +1,45 @@ +/********************* */ +/*! \file first_order_reasoning.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-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process step for first-order reasoning + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__FIRST_ORDER_REASONING_H +#define __CVC4__FIRST_ORDER_REASONING_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class FirstOrderPropagation { +private: + std::map< Node, Node > d_const_def; + std::map< Node, bool > d_assertion_true; + Node process(Node a, std::vector< Node > & lits); + void collectLits( Node n, std::vector<Node> & lits ); + Node simplify( Node n ); +public: + FirstOrderPropagation(){} + ~FirstOrderPropagation(){} + + void simplify( std::vector< Node >& assertions ); +}; + +} + +#endif diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp new file mode 100644 index 000000000..bf10369e6 --- /dev/null +++ b/src/theory/quantifiers/full_model_check.cpp @@ -0,0 +1,1409 @@ +/********************* */ +/*! \file full_model_check.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of full model check class + **/ + +#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/options.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::theory::inst; +using namespace CVC4::theory::quantifiers::fmcheck; + +struct ModelBasisArgSort +{ + std::vector< Node > d_terms; + bool operator() (int i,int j) { + return (d_terms[i].getAttribute(ModelBasisArgAttribute()) < + d_terms[j].getAttribute(ModelBasisArgAttribute()) ); + } +}; + + +struct ConstRationalSort +{ + std::vector< Node > d_terms; + bool operator() (int i, int j) { + return (d_terms[i].getConst<Rational>() < d_terms[j].getConst<Rational>() ); + } +}; + + +bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { + if (index==(int)c.getNumChildren()) { + return d_data!=-1; + }else{ + TypeNode tn = c[index].getType(); + Node st = m->getStar(tn); + if(d_child.find(st)!=d_child.end()) { + if( d_child[st].hasGeneralization(m, c, index+1) ){ + return true; + } + } + if( c[index]!=st && d_child.find( c[index] )!=d_child.end() ){ + if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){ + return true; + } + } + if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){ + //for star: check if all children are defined and have generalizations + if( options::fmfFmcCoverSimplify() && c[index]==st ){ + //check if all children exist and are complete + int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0); + if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){ + bool complete = true; + for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){ + if( !m->isStar(it->first) ){ + if( !it->second.hasGeneralization(m, c, index+1) ){ + complete = false; + break; + } + } + } + if( complete ){ + return true; + } + } + } + } + + return false; + } +} + +int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) { + Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl; + if (index==(int)inst.size()) { + return d_data; + }else{ + int minIndex = -1; + if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){ + for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){ + if( !m->isInterval( it->first ) ){ + std::cout << "Not an interval during getGenIndex " << it->first << std::endl; + exit( 11 ); + } + //check if it is in the range + if( m->isInRange(inst[index], it->first ) ){ + int gindex = it->second.getGeneralizationIndex(m, inst, index+1); + if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){ + minIndex = gindex; + } + } + } + }else{ + Node st = m->getStar(inst[index].getType()); + if(d_child.find(st)!=d_child.end()) { + minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1); + } + Node cc = inst[index]; + if( cc!=st && d_child.find( cc )!=d_child.end() ){ + int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1); + if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){ + minIndex = gindex; + } + } + } + return minIndex; + } +} + +void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) { + if (index==(int)c.getNumChildren()) { + if(d_data==-1) { + d_data = data; + } + } + else { + d_child[ c[index] ].addEntry(m,c,v,data,index+1); + if( d_complete==0 ){ + d_complete = -1; + } + } +} + +void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) { + if (index==(int)c.getNumChildren()) { + if( d_data!=-1) { + if( is_gen ){ + gen.push_back(d_data); + } + compat.push_back(d_data); + } + }else{ + if (m->isStar(c[index])) { + for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){ + it->second.getEntries(m, c, compat, gen, index+1, is_gen ); + } + }else{ + Node st = m->getStar(c[index].getType()); + if(d_child.find(st)!=d_child.end()) { + d_child[st].getEntries(m, c, compat, gen, index+1, false); + } + if( d_child.find( c[index] )!=d_child.end() ){ + d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen); + } + } + + } +} + +void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) { + if (index==(int)c.getNumChildren()) { + if( d_data!=-1 ){ + indices.push_back( d_data ); + } + }else{ + for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){ + it->second.collectIndices(c, index+1, indices ); + } + } +} + +bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) { + if( d_complete==-1 ){ + d_complete = 1; + if (index<(int)c.getNumChildren()) { + Node st = m->getStar(c[index].getType()); + if(d_child.find(st)!=d_child.end()) { + if (!d_child[st].isComplete(m, c, index+1)) { + d_complete = 0; + } + }else{ + d_complete = 0; + } + } + } + return d_complete==1; +} + +bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) { + if (d_et.hasGeneralization(m, c)) { + Trace("fmc-debug") << "Already has generalization, skip." << std::endl; + return false; + } + int newIndex = (int)d_cond.size(); + if (!d_has_simplified) { + std::vector<int> compat; + std::vector<int> gen; + d_et.getEntries(m, c, compat, gen); + for( unsigned i=0; i<compat.size(); i++) { + if( d_status[compat[i]]==status_unk ){ + if( d_value[compat[i]]!=v ){ + d_status[compat[i]] = status_non_redundant; + } + } + } + for( unsigned i=0; i<gen.size(); i++) { + if( d_status[gen[i]]==status_unk ){ + if( d_value[gen[i]]==v ){ + d_status[gen[i]] = status_redundant; + } + } + } + d_status.push_back( status_unk ); + } + d_et.addEntry(m, c, v, newIndex); + d_cond.push_back(c); + d_value.push_back(v); + return true; +} + +Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) { + int gindex = d_et.getGeneralizationIndex(m, inst); + if (gindex!=-1) { + return d_value[gindex]; + }else{ + Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl; + return Node::null(); + } +} + +int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) { + return d_et.getGeneralizationIndex(m, inst); +} + +void Def::basic_simplify( FirstOrderModelFmc * m ) { + d_has_simplified = true; + std::vector< Node > cond; + cond.insert( cond.end(), d_cond.begin(), d_cond.end() ); + d_cond.clear(); + std::vector< Node > value; + value.insert( value.end(), d_value.begin(), d_value.end() ); + d_value.clear(); + d_et.reset(); + for (unsigned i=0; i<d_status.size(); i++) { + if( d_status[i]!=status_redundant ){ + addEntry(m, cond[i], value[i]); + } + } + d_status.clear(); +} + +void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) { + basic_simplify( m ); + + //check if the last entry is not all star, if so, we can make the last entry all stars + if( !d_cond.empty() ){ + bool last_all_stars = true; + Node cc = d_cond[d_cond.size()-1]; + for( unsigned i=0; i<cc.getNumChildren(); i++ ){ + if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){ + last_all_stars = false; + break; + } + } + if( !last_all_stars ){ + Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl; + Trace("fmc-cover-simplify") << "Before: " << std::endl; + debugPrint("fmc-cover-simplify",Node::null(), mc); + Trace("fmc-cover-simplify") << std::endl; + std::vector< Node > cond; + cond.insert( cond.end(), d_cond.begin(), d_cond.end() ); + d_cond.clear(); + std::vector< Node > value; + value.insert( value.end(), d_value.begin(), d_value.end() ); + d_value.clear(); + d_et.reset(); + d_has_simplified = false; + //change the last to all star + std::vector< Node > nc; + nc.push_back( cc.getOperator() ); + for( unsigned j=0; j< cc.getNumChildren(); j++){ + nc.push_back(m->getStarElement(cc[j].getType())); + } + cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc ); + //re-add the entries + for (unsigned i=0; i<cond.size(); i++) { + addEntry(m, cond[i], value[i]); + } + Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl; + basic_simplify( m ); + Trace("fmc-cover-simplify") << "After: " << std::endl; + debugPrint("fmc-cover-simplify",Node::null(), mc); + Trace("fmc-cover-simplify") << std::endl; + } + } +} + +void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { + if (!op.isNull()) { + Trace(tr) << "Model for " << op << " : " << std::endl; + } + for( unsigned i=0; i<d_cond.size(); i++) { + //print the condition + if (!op.isNull()) { + Trace(tr) << op; + } + m->debugPrintCond(tr, d_cond[i], true); + Trace(tr) << " -> "; + m->debugPrint(tr, d_value[i]); + Trace(tr) << std::endl; + } +} + + +FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) : +QModelBuilder( c, qe ){ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +bool FullModelChecker::optBuildAtFullModel() { + //need to build after full model has taken effect if we are constructing interval models + // this is because we need to have a constant in all integer equivalence classes + return options::fmfFmcInterval(); +} + +void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ + FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); + if( fullModel==optBuildAtFullModel() ){ + Trace("fmc") << "---Full Model Check reset() " << std::endl; + fm->initialize( d_considerAxioms ); + d_quant_models.clear(); + d_rep_ids.clear(); + d_star_insts.clear(); + //process representatives + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); + it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first); + Node rmbt = fm->getUsedRepresentative( mbt); + int mbt_index = -1; + Trace("fmc") << " Model basis term : " << mbt << std::endl; + for( size_t a=0; a<it->second.size(); a++ ){ + Node r = fm->getUsedRepresentative( it->second[a] ); + std::vector< Node > eqc; + ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); + Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt); + Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; + //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; + Trace("fmc-model-debug") << " {"; + //find best selection for representative + for( size_t i=0; i<eqc.size(); i++ ){ + Trace("fmc-model-debug") << eqc[i] << ", "; + } + Trace("fmc-model-debug") << "}" << std::endl; + + //if this is the model basis eqc, replace with actual model basis term + if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) { + fm->d_model_basis_rep[it->first] = r; + r = mbt; + mbt_index = a; + } + d_rep_ids[it->first][r] = (int)a; + } + Trace("fmc-model-debug") << std::endl; + + if (mbt_index==-1) { + std::cout << " WARNING: model basis term is not a representative!" << std::endl; + exit(0); + }else{ + Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl; + } + } + } + //also process non-rep set sorts + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + for( unsigned i=0; i<tno.getNumChildren(); i++) { + initializeType( fm, tno[i] ); + } + } + //now, make models + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + //reset the model + fm->d_models[op]->reset(); + + Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl; + for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ + Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]); + Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl; + } + Trace("fmc-model-debug") << std::endl; + + + std::vector< Node > add_conds; + std::vector< Node > add_values; + bool needsDefault = true; + for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ + Node n = fm->d_uf_terms[op][i]; + if( !n.getAttribute(NoMatchAttribute()) ){ + add_conds.push_back( n ); + add_values.push_back( n ); + } + } + //possibly get default + if( needsDefault ){ + Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op); + //add default value if necessary + if( fm->hasTerm( nmb ) ){ + Trace("fmc-model-debug") << "Add default " << nmb << std::endl; + add_conds.push_back( nmb ); + add_values.push_back( nmb ); + }else{ + Node vmb = getSomeDomainElement(fm, nmb.getType()); + Trace("fmc-model-debug") << "Add default to default representative " << nmb << " "; + Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl; + add_conds.push_back( nmb ); + add_values.push_back( vmb ); + } + } + + std::vector< Node > conds; + std::vector< Node > values; + std::vector< Node > entry_conds; + //get the entries for the mdoel + for( size_t i=0; i<add_conds.size(); i++ ){ + Node c = add_conds[i]; + Node v = add_values[i]; + std::vector< Node > children; + std::vector< Node > entry_children; + children.push_back(op); + entry_children.push_back(op); + bool hasNonStar = false; + for( unsigned i=0; i<c.getNumChildren(); i++) { + Node ri = fm->getUsedRepresentative( c[i]); + if( !ri.getType().isSort() && !ri.isConst() ){ + Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; + } + children.push_back(ri); + if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){ + if (fm->isModelBasisTerm(ri) ) { + ri = fm->getStar( ri.getType() ); + }else{ + hasNonStar = true; + } + } + entry_children.push_back(ri); + } + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + Node nv = fm->getUsedRepresentative( v ); + if( !nv.getType().isSort() && !nv.isConst() ){ + Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; + } + Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); + if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ + Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; + conds.push_back(n); + values.push_back(nv); + entry_conds.push_back(en); + } + else { + Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; + } + } + + + //sort based on # default arguments + std::vector< int > indices; + ModelBasisArgSort mbas; + for (int i=0; i<(int)conds.size(); i++) { + d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] ); + mbas.d_terms.push_back(conds[i]); + indices.push_back(i); + } + std::sort( indices.begin(), indices.end(), mbas ); + + for (int i=0; i<(int)indices.size(); i++) { + fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]); + } + + + if( options::fmfFmcInterval() ){ + Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl; + fm->d_models[op]->debugPrint("fmc-interval-model", op, this); + Trace("fmc-interval-model") << std::endl; + std::vector< int > indices; + for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){ + indices.push_back( i ); + } + std::map< int, std::map< int, Node > > changed_vals; + makeIntervalModel( fm, op, indices, 0, changed_vals ); + + std::vector< Node > conds; + std::vector< Node > values; + for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){ + if( changed_vals.find(i)==changed_vals.end() ){ + conds.push_back( fm->d_models[op]->d_cond[i] ); + }else{ + std::vector< Node > children; + children.push_back( op ); + for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){ + if( changed_vals[i].find(j)==changed_vals[i].end() ){ + children.push_back( fm->d_models[op]->d_cond[i][j] ); + }else{ + children.push_back( changed_vals[i][j] ); + } + } + Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + conds.push_back( nc ); + Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to "; + debugPrintCond("fmc-interval-model", nc, true ); + Trace("fmc-interval-model") << std::endl; + } + values.push_back( fm->d_models[op]->d_value[i] ); + } + fm->d_models[op]->reset(); + for( unsigned i=0; i<conds.size(); i++ ){ + fm->d_models[op]->addEntry(fm, conds[i], values[i] ); + } + } + + Trace("fmc-model-simplify") << "Before simplification : " << std::endl; + fm->d_models[op]->debugPrint("fmc-model-simplify", op, this); + Trace("fmc-model-simplify") << std::endl; + + Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl; + fm->d_models[op]->simplify( this, fm ); + + fm->d_models[op]->debugPrint("fmc-model", op, this); + Trace("fmc-model") << std::endl; + } + } + if( fullModel ){ + //make function values + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){ + m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" ); + } + TheoryEngineModelBuilder::processBuildModel( m, fullModel ); + //mark that the model has been set + fm->markModelSet(); + //debug the model + debugModel( fm ); + } +} + +void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){ + if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){ + Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl; + Node mbn; + if (!fm->d_rep_set.hasType(tn)) { + mbn = fm->getSomeDomainElement(tn); + }else{ + mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); + } + Node mbnr = fm->getUsedRepresentative( mbn ); + fm->d_model_basis_rep[tn] = mbnr; + Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; + } +} + +void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) { + Trace(tr) << "("; + for( unsigned j=0; j<n.getNumChildren(); j++) { + if( j>0 ) Trace(tr) << ", "; + debugPrint(tr, n[j], dispStar); + } + Trace(tr) << ")"; +} + +void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { + FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel(); + if( n.isNull() ){ + Trace(tr) << "null"; + } + else if(fm->isStar(n) && dispStar) { + Trace(tr) << "*"; + } + else if(fm->isInterval(n)) { + debugPrint(tr, n[0], dispStar ); + Trace(tr) << "..."; + debugPrint(tr, n[1], dispStar ); + }else{ + TypeNode tn = n.getType(); + if( d_rep_ids.find(tn)!=d_rep_ids.end() ){ + if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) { + Trace(tr) << d_rep_ids[tn][n]; + }else{ + Trace(tr) << n; + } + }else{ + Trace(tr) << n; + } + } +} + + +bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { + Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; + if( optUseModel() ){ + FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc(); + if (effort==0) { + //register the quantifier + if (d_quant_cond.find(f)==d_quant_cond.end()) { + std::vector< TypeNode > types; + for(unsigned i=0; i<f[0].getNumChildren(); i++){ + types.push_back(f[0][i].getType()); + d_quant_var_id[f][f[0][i]] = i; + } + TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() ); + Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); + d_quant_cond[f] = op; + } + //make sure all types are set + for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ + initializeType( fmfmc, f[0][i].getType() ); + } + + //model check the quantifier + doCheck(fmfmc, f, d_quant_models[f], f[1]); + Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; + d_quant_models[f].debugPrint("fmc", Node::null(), this); + Trace("fmc") << std::endl; + + //consider all entries going to non-true + for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) { + if( d_quant_models[f].d_value[i]!=d_true) { + Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl; + bool hasStar = false; + std::vector< Node > inst; + for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) { + if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) { + hasStar = true; + inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType())); + }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){ + hasStar = true; + //if interval, find a sample point + if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){ + if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){ + inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType())); + }else{ + Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1], + NodeManager::currentNM()->mkConst( Rational(1) ) ); + nn = Rewriter::rewrite( nn ); + inst.push_back( nn ); + } + }else{ + inst.push_back(d_quant_models[f].d_cond[i][j][0]); + } + }else{ + inst.push_back(d_quant_models[f].d_cond[i][j]); + } + } + bool addInst = true; + if( hasStar ){ + //try obvious (specified by inst) + Node ev = d_quant_models[f].evaluate(fmfmc, inst); + if (ev==d_true) { + addInst = false; + } + }else{ + //for debugging + if (Trace.isOn("fmc-test-inst")) { + Node ev = d_quant_models[f].evaluate(fmfmc, inst); + if( ev==d_true ){ + std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl; + exit(0); + }else{ + Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl; + } + } + } + if( addInst ){ + InstMatch m; + for( unsigned j=0; j<inst.size(); j++) { + m.set( d_qe, f, j, inst[j] ); + } + d_triedLemmas++; + if( d_qe->addInstantiation( f, m ) ){ + Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; + d_addedLemmas++; + }else{ + Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl; + //this can happen if evaluation is unknown + //might try it next effort level + d_star_insts[f].push_back(i); + } + }else{ + Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl; + //might try it next effort level + d_star_insts[f].push_back(i); + } + } + } + }else{ + if (!d_star_insts[f].empty()) { + Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl; + Trace("fmc-exh") << "Definition was : " << std::endl; + d_quant_models[f].debugPrint("fmc-exh", Node::null(), this); + Trace("fmc-exh") << std::endl; + Def temp; + //simplify the exceptions? + for( int i=(d_star_insts[f].size()-1); i>=0; i--) { + //get witness for d_star_insts[f][i] + int j = d_star_insts[f][i]; + if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ + if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){ + //something went wrong, resort to exhaustive instantiation + return false; + } + } + } + } + } + return true; + }else{ + return false; + } +} + +bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) { + RepSetIterator riter( d_qe, &(fm->d_rep_set) ); + Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " "; + debugPrintCond("fmc-exh", c, true); + Trace("fmc-exh")<< std::endl; + Trace("fmc-exh-debug") << "Set interval domains..." << std::endl; + //set the bounds on the iterator based on intervals + for( unsigned i=0; i<c.getNumChildren(); i++ ){ + if( c[i].getType().isInteger() ){ + if( fm->isInterval(c[i]) ){ + for( unsigned b=0; b<2; b++ ){ + if( !fm->isStar(c[i][b]) ){ + riter.d_bounds[b][i] = c[i][b]; + } + } + }else if( !fm->isStar(c[i]) ){ + riter.d_bounds[0][i] = c[i]; + riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 ); + } + } + } + Trace("fmc-exh-debug") << "Set quantifier..." << std::endl; + //initialize + if( riter.setQuantifier( f ) ){ + Trace("fmc-exh-debug") << "Set element domains..." << std::endl; + //set the domains based on the entry + for (unsigned i=0; i<c.getNumChildren(); i++) { + if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) { + TypeNode tn = c[i].getType(); + if( d_rep_ids.find(tn)!=d_rep_ids.end() ){ + if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){ + //add the full range + }else{ + if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) { + riter.d_domain[i].clear(); + riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]); + }else{ + return false; + } + } + }else{ + return false; + } + } + } + int addedLemmas = 0; + //now do full iteration + while( !riter.isFinished() ){ + d_triedLemmas++; + Trace("fmc-exh-debug") << "Inst : "; + std::vector< Node > inst; + for( int i=0; i<riter.getNumTerms(); i++ ){ + //m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) ); + Node r = fm->getUsedRepresentative( riter.getTerm( i ) ); + debugPrint("fmc-exh-debug", r); + Trace("fmc-exh-debug") << " "; + inst.push_back(r); + } + int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst); + Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size(); + Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index]; + if (ev!=d_true) { + InstMatch m; + for( int i=0; i<riter.getNumTerms(); i++ ){ + m.set( d_qe, f, i, riter.getTerm( i ) ); + } + Trace("fmc-exh-debug") << ", add!"; + //add as instantiation + if( d_qe->addInstantiation( f, m ) ){ + Trace("fmc-exh-debug") << " ...success."; + addedLemmas++; + } + }else{ + Trace("fmc-exh-debug") << ", already true"; + } + Trace("fmc-exh-debug") << std::endl; + int index = riter.increment(); + Trace("fmc-exh-debug") << "Incremented index " << index << std::endl; + if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) { + Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl; + riter.increment2( index-1 ); + } + } + d_addedLemmas += addedLemmas; + return true; + }else{ + return false; + } +} + +void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) { + Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl; + //first check if it is a bounding literal + if( n.hasAttribute(BoundIntLitAttribute()) ){ + Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl; + d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true ); + }else if( n.getKind() == kind::BOUND_VARIABLE ){ + Trace("fmc-debug") << "Add default entry..." << std::endl; + d.addEntry(fm, mkCondDefault(fm, f), n); + } + else if( n.getKind() == kind::NOT ){ + //just do directly + doCheck( fm, f, d, n[0] ); + doNegate( d ); + } + else if( n.getKind() == kind::FORALL ){ + d.addEntry(fm, mkCondDefault(fm, f), Node::null()); + } + else if( n.getType().isArray() ){ + //make the definition + Node r = fm->getRepresentative(n); + Trace("fmc-debug") << "Representative for array is " << r << std::endl; + while( r.getKind() == kind::STORE ){ + Node i = fm->getUsedRepresentative( r[1] ); + Node e = fm->getUsedRepresentative( r[2] ); + d.addEntry(fm, mkArrayCond(i), e ); + r = fm->getRepresentative( r[0] ); + } + Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType())); + bool success = false; + Node odefaultValue; + if( r.getKind() == kind::STORE_ALL ){ + ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>(); + odefaultValue = Node::fromExpr(storeAll.getExpr()); + Node defaultValue = fm->getUsedRepresentative( odefaultValue, true ); + if( !defaultValue.isNull() ){ + d.addEntry(fm, defC, defaultValue); + success = true; + } + } + if( !success ){ + Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl; + Trace("fmc-warn") << " Default value was : " << odefaultValue << std::endl; + Trace("fmc-debug") << "Can't process base array " << r << std::endl; + //can't process this array + d.reset(); + d.addEntry(fm, defC, Node::null()); + } + } + else if( n.getNumChildren()==0 ){ + Node r = n; + if( !n.isConst() ){ + if( !fm->hasTerm(n) ){ + r = getSomeDomainElement(fm, n.getType() ); + } + r = fm->getUsedRepresentative( r ); + } + Trace("fmc-debug") << "Add constant entry..." << std::endl; + d.addEntry(fm, mkCondDefault(fm, f), r); + } + else{ + std::vector< int > var_ch; + std::vector< Def > children; + for( int i=0; i<(int)n.getNumChildren(); i++) { + Def dc; + doCheck(fm, f, dc, n[i]); + children.push_back(dc); + if( n[i].getKind() == kind::BOUND_VARIABLE ){ + var_ch.push_back(i); + } + } + + if( n.getKind()==APPLY_UF ){ + Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl; + //uninterpreted compose + doUninterpretedCompose( fm, f, d, n.getOperator(), children ); + } else if( n.getKind()==SELECT ){ + Trace("fmc-debug") << "Do select compose " << n << std::endl; + std::vector< Def > children2; + children2.push_back( children[1] ); + std::vector< Node > cond; + mkCondDefaultVec(fm, f, cond); + std::vector< Node > val; + doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val ); + } else { + if( !var_ch.empty() ){ + if( n.getKind()==EQUAL ){ + if( var_ch.size()==2 ){ + Trace("fmc-debug") << "Do variable equality " << n << std::endl; + doVariableEquality( fm, f, d, n ); + }else{ + Trace("fmc-debug") << "Do variable relation " << n << std::endl; + doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] ); + } + }else{ + Trace("fmc-warn") << "Don't know how to check " << n << std::endl; + d.addEntry(fm, mkCondDefault(fm, f), Node::null()); + } + }else{ + Trace("fmc-debug") << "Do interpreted compose " << n << std::endl; + std::vector< Node > cond; + mkCondDefaultVec(fm, f, cond); + std::vector< Node > val; + //interpreted compose + doInterpretedCompose( fm, f, d, n, children, 0, cond, val ); + } + } + Trace("fmc-debug") << "Simplify the definition..." << std::endl; + d.debugPrint("fmc-debug", Node::null(), this); + d.simplify(this, fm); + Trace("fmc-debug") << "Done simplifying" << std::endl; + } + Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl; + d.debugPrint("fmc-debug", Node::null(), this); + Trace("fmc-debug") << std::endl; +} + +void FullModelChecker::doNegate( Def & dc ) { + for (unsigned i=0; i<dc.d_cond.size(); i++) { + if (!dc.d_value[i].isNull()) { + dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true; + } + } +} + +void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) { + std::vector<Node> cond; + mkCondDefaultVec(fm, f, cond); + if (eq[0]==eq[1]){ + d.addEntry(fm, mkCond(cond), d_true); + }else{ + TypeNode tn = eq[0].getType(); + if( tn.isSort() ){ + int j = getVariableId(f, eq[0]); + int k = getVariableId(f, eq[1]); + if( !fm->d_rep_set.hasType( tn ) ){ + getSomeDomainElement( fm, tn ); //to verify the type is initialized + } + for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) { + Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] ); + cond[j+1] = r; + cond[k+1] = r; + d.addEntry( fm, mkCond(cond), d_true); + } + d.addEntry( fm, mkCondDefault(fm, f), d_false); + }else{ + d.addEntry( fm, mkCondDefault(fm, f), Node::null()); + } + } +} + +void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) { + int j = getVariableId(f, v); + for (unsigned i=0; i<dc.d_cond.size(); i++) { + Node val = dc.d_value[i]; + if( val.isNull() ){ + d.addEntry( fm, dc.d_cond[i], val); + }else{ + if( dc.d_cond[i][j]!=val ){ + if (fm->isStar(dc.d_cond[i][j])) { + std::vector<Node> cond; + mkCondVec(dc.d_cond[i],cond); + cond[j+1] = val; + d.addEntry(fm, mkCond(cond), d_true); + cond[j+1] = fm->getStar(val.getType()); + d.addEntry(fm, mkCond(cond), d_false); + }else{ + d.addEntry( fm, dc.d_cond[i], d_false); + } + }else{ + d.addEntry( fm, dc.d_cond[i], d_true); + } + } + } +} + +void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) { + Trace("fmc-uf-debug") << "Definition : " << std::endl; + fm->d_models[op]->debugPrint("fmc-uf-debug", op, this); + Trace("fmc-uf-debug") << std::endl; + + std::vector< Node > cond; + mkCondDefaultVec(fm, f, cond); + std::vector< Node > val; + doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val); +} + +void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, + Def & df, std::vector< Def > & dc, int index, + std::vector< Node > & cond, std::vector<Node> & val ) { + Trace("fmc-uf-process") << "process at " << index << std::endl; + for( unsigned i=1; i<cond.size(); i++) { + debugPrint("fmc-uf-process", cond[i], true); + Trace("fmc-uf-process") << " "; + } + Trace("fmc-uf-process") << std::endl; + if (index==(int)dc.size()) { + //we have an entry, now do actual compose + std::map< int, Node > entries; + doUninterpretedCompose2( fm, f, entries, 0, cond, val, df.d_et); + if( entries.empty() ){ + d.addEntry(fm, mkCond(cond), Node::null()); + }else{ + //add them to the definition + for( unsigned e=0; e<df.d_cond.size(); e++ ){ + if ( entries.find(e)!=entries.end() ){ + Trace("fmf-uf-process-debug") << "Add entry..." << std::endl; + d.addEntry(fm, entries[e], df.d_value[e] ); + Trace("fmf-uf-process-debug") << "Done add entry." << std::endl; + } + } + } + }else{ + for (unsigned i=0; i<dc[index].d_cond.size(); i++) { + if (isCompat(fm, cond, dc[index].d_cond[i])!=0) { + std::vector< Node > new_cond; + new_cond.insert(new_cond.end(), cond.begin(), cond.end()); + if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){ + Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl; + val.push_back(dc[index].d_value[i]); + doUninterpretedCompose(fm, f, d, df, dc, index+1, new_cond, val); + val.pop_back(); + }else{ + Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl; + } + } + } + } +} + +void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, + std::map< int, Node > & entries, int index, + std::vector< Node > & cond, std::vector< Node > & val, + EntryTrie & curr ) { + Trace("fmc-uf-process") << "compose " << index << std::endl; + for( unsigned i=1; i<cond.size(); i++) { + debugPrint("fmc-uf-process", cond[i], true); + Trace("fmc-uf-process") << " "; + } + Trace("fmc-uf-process") << std::endl; + if (index==(int)val.size()) { + Node c = mkCond(cond); + Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl; + entries[curr.d_data] = c; + }else{ + Node v = val[index]; + bool bind_var = false; + if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){ + int j = getVariableId(f, v); + Trace("fmc-uf-process") << v << " is variable #" << j << std::endl; + if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) { + v = cond[j+1]; + }else{ + bind_var = true; + } + } + if (bind_var) { + Trace("fmc-uf-process") << "bind variable..." << std::endl; + int j = getVariableId(f, v); + if( fm->isStar(cond[j+1]) ){ + for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { + cond[j+1] = it->first; + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); + } + cond[j+1] = fm->getStar(v.getType()); + }else{ + Node orig = cond[j+1]; + for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { + Node nw = doIntervalMeet( fm, it->first, orig ); + if( !nw.isNull() ){ + cond[j+1] = nw; + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); + } + } + cond[j+1] = orig; + } + }else{ + if( !v.isNull() ){ + if( options::fmfFmcInterval() && v.getType().isInteger() ){ + for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { + if( fm->isInRange( v, it->first ) ){ + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); + } + } + }else{ + if (curr.d_child.find(v)!=curr.d_child.end()) { + Trace("fmc-uf-process") << "follow value..." << std::endl; + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]); + } + Node st = fm->getStarElement(v.getType()); + if (curr.d_child.find(st)!=curr.d_child.end()) { + Trace("fmc-uf-process") << "follow star..." << std::endl; + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]); + } + } + } + } + } +} + +void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, + std::vector< Def > & dc, int index, + std::vector< Node > & cond, std::vector<Node> & val ) { + if ( index==(int)dc.size() ){ + Node c = mkCond(cond); + Node v = evaluateInterpreted(n, val); + d.addEntry(fm, c, v); + } + else { + TypeNode vtn = n.getType(); + for (unsigned i=0; i<dc[index].d_cond.size(); i++) { + if (isCompat(fm, cond, dc[index].d_cond[i])!=0) { + std::vector< Node > new_cond; + new_cond.insert(new_cond.end(), cond.begin(), cond.end()); + if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){ + bool process = true; + if (vtn.isBoolean()) { + //short circuit + if( (n.getKind()==OR && dc[index].d_value[i]==d_true) || + (n.getKind()==AND && dc[index].d_value[i]==d_false) ){ + Node c = mkCond(new_cond); + d.addEntry(fm, c, dc[index].d_value[i]); + process = false; + } + } + if (process) { + val.push_back(dc[index].d_value[i]); + doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val); + val.pop_back(); + } + } + } + } + } +} + +int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) { + Trace("fmc-debug3") << "isCompat " << c << std::endl; + Assert(cond.size()==c.getNumChildren()+1); + for (unsigned i=1; i<cond.size(); i++) { + if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){ + Node iv = doIntervalMeet( fm, cond[i], c[i-1], false ); + if( iv.isNull() ){ + return 0; + } + }else{ + if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) { + return 0; + } + } + } + return 1; +} + +bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) { + Trace("fmc-debug3") << "doMeet " << c << std::endl; + Assert(cond.size()==c.getNumChildren()+1); + for (unsigned i=1; i<cond.size(); i++) { + if( cond[i]!=c[i-1] ) { + if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){ + Node iv = doIntervalMeet( fm, cond[i], c[i-1] ); + if( !iv.isNull() ){ + cond[i] = iv; + }else{ + return false; + } + }else{ + if( fm->isStar(cond[i]) ){ + cond[i] = c[i-1]; + }else if( !fm->isStar(c[i-1]) ){ + return false; + } + } + } + } + return true; +} + +Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) { + if( fm->isStar( i1 ) ){ + return i2; + }else if( fm->isStar( i2 ) ){ + return i1; + }else{ + if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){ + std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl; + exit( 0 ); + } + Node b[2]; + for( unsigned j=0; j<2; j++ ){ + Node b1 = i1[j]; + Node b2 = i2[j]; + if( fm->isStar( b1 ) ){ + b[j] = b2; + }else if( fm->isStar( b2 ) ){ + b[j] = b1; + }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){ + b[j] = j==0 ? b2 : b1; + }else{ + b[j] = j==0 ? b1 : b2; + } + } + if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){ + return mk ? fm->getInterval( b[0], b[1] ) : i1; + }else{ + return Node::null(); + } + } +} + +Node FullModelChecker::mkCond( std::vector< Node > & cond ) { + return NodeManager::currentNM()->mkNode(APPLY_UF, cond); +} + +Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) { + std::vector< Node > cond; + mkCondDefaultVec(fm, f, cond); + return mkCond(cond); +} + +void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) { + Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl; + //get function symbol for f + cond.push_back(d_quant_cond[f]); + for (unsigned i=0; i<f[0].getNumChildren(); i++) { + Node ts = fm->getStarElement( f[0][i].getType() ); + cond.push_back(ts); + } +} + +void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) { + cond.push_back(n.getOperator()); + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + cond.push_back( n[i] ); + } +} + +Node FullModelChecker::mkArrayCond( Node a ) { + if( d_array_term_cond.find(a)==d_array_term_cond.end() ){ + if( d_array_cond.find(a.getType())==d_array_cond.end() ){ + TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() ); + Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); + d_array_cond[a.getType()] = op; + } + std::vector< Node > cond; + cond.push_back(d_array_cond[a.getType()]); + cond.push_back(a); + d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond ); + } + return d_array_term_cond[a]; +} + +Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) { + if( n.getKind()==EQUAL ){ + if (!vals[0].isNull() && !vals[1].isNull()) { + return vals[0]==vals[1] ? d_true : d_false; + }else{ + return Node::null(); + } + }else if( n.getKind()==ITE ){ + if( vals[0]==d_true ){ + return vals[1]; + }else if( vals[0]==d_false ){ + return vals[2]; + }else{ + return vals[1]==vals[2] ? vals[1] : Node::null(); + } + }else if( n.getKind()==AND || n.getKind()==OR ){ + bool isNull = false; + for (unsigned i=0; i<vals.size(); i++) { + if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) { + return vals[i]; + }else if( vals[i].isNull() ){ + isNull = true; + } + } + return isNull ? Node::null() : vals[0]; + }else{ + std::vector<Node> children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for (unsigned i=0; i<vals.size(); i++) { + if( vals[i].isNull() ){ + return Node::null(); + }else{ + children.push_back( vals[i] ); + } + } + Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children); + Trace("fmc-eval") << "Evaluate " << nc << " to "; + nc = Rewriter::rewrite(nc); + Trace("fmc-eval") << nc << std::endl; + return nc; + } +} + +Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) { + bool addRepId = !fm->d_rep_set.hasType( tn ); + Node de = fm->getSomeDomainElement(tn); + if( addRepId ){ + d_rep_ids[tn][de] = 0; + } + return de; +} + +Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) { + return fm->getFunctionValue(op, argPrefix); +} + + +bool FullModelChecker::useSimpleModels() { + return options::fmfFmcSimple(); +} + +void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, + std::map< int, std::map< int, Node > >& changed_vals ) { + if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){ + makeIntervalModel2( fm, op, indices, 0, changed_vals ); + }else{ + TypeNode tn = fm->d_models[op]->d_cond[0][index].getType(); + if( tn.isInteger() ){ + makeIntervalModel(fm,op,indices,index+1, changed_vals ); + }else{ + std::map< Node, std::vector< int > > new_indices; + for( unsigned i=0; i<indices.size(); i++ ){ + Node v = fm->d_models[op]->d_cond[indices[i]][index]; + new_indices[v].push_back( indices[i] ); + } + + for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){ + makeIntervalModel( fm, op, it->second, index+1, changed_vals ); + } + } + } +} + +void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, + std::map< int, std::map< int, Node > >& changed_vals ) { + Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : "; + for( unsigned i=0; i<indices.size(); i++ ){ + Debug("fmc-interval-model-debug") << indices[i] << " "; + } + Debug("fmc-interval-model-debug") << std::endl; + + if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){ + TypeNode tn = fm->d_models[op]->d_cond[0][index].getType(); + if( tn.isInteger() ){ + std::map< Node, std::vector< int > > new_indices; + for( unsigned i=0; i<indices.size(); i++ ){ + Node v = fm->d_models[op]->d_cond[indices[i]][index]; + new_indices[v].push_back( indices[i] ); + if( !v.isConst() ){ + Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl; + Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl; + } + } + + std::vector< Node > values; + for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){ + makeIntervalModel2( fm, op, it->second, index+1, changed_vals ); + values.push_back( it->first ); + } + + if( tn.isInteger() ){ + //sort values by size + ConstRationalSort crs; + std::vector< int > sindices; + for( unsigned i=0; i<values.size(); i++ ){ + sindices.push_back( (int)i ); + crs.d_terms.push_back( values[i] ); + } + std::sort( sindices.begin(), sindices.end(), crs ); + + Node ub = fm->getStar( tn ); + for( int i=(int)(sindices.size()-1); i>=0; i-- ){ + Node lb = fm->getStar( tn ); + if( i>0 ){ + lb = values[sindices[i]]; + } + Node interval = fm->getInterval( lb, ub ); + for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){ + Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl; + changed_vals[new_indices[values[sindices[i]]][j]][index] = interval; + } + ub = lb; + } + } + }else{ + makeIntervalModel2( fm, op, indices, index+1, changed_vals ); + } + } +} diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h new file mode 100644 index 000000000..6bb375c34 --- /dev/null +++ b/src/theory/quantifiers/full_model_check.h @@ -0,0 +1,160 @@ +/********************* */ +/*! \file full_model_check.h + ** \verbatim + ** Original author: Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Full model check class + **/ + +#include "cvc4_private.h" + +#ifndef FULL_MODEL_CHECK +#define FULL_MODEL_CHECK + +#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { +namespace fmcheck { + + +class FirstOrderModelFmc; +class FullModelChecker; + +class EntryTrie +{ +private: + int d_complete; +public: + EntryTrie() : d_complete(-1), d_data(-1){} + std::map<Node,EntryTrie> d_child; + int d_data; + void reset() { d_data = -1; d_child.clear(); d_complete = -1; } + void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 ); + bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 ); + int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 ); + void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true ); + + void collectIndices(Node c, int index, std::vector< int >& indices ); + bool isComplete(FirstOrderModelFmc * m, Node c, int index); +}; + + +class Def +{ +public: + EntryTrie d_et; + //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative + std::vector< Node > d_cond; + //value is returned by FullModelChecker::getRepresentative + std::vector< Node > d_value; + void basic_simplify( FirstOrderModelFmc * m ); +private: + enum { + status_unk, + status_redundant, + status_non_redundant + }; + std::vector< int > d_status; + bool d_has_simplified; +public: + Def() : d_has_simplified(false){} + void reset() { + d_et.reset(); + d_cond.clear(); + d_value.clear(); + d_status.clear(); + d_has_simplified = false; + } + bool addEntry( FirstOrderModelFmc * m, Node c, Node v); + Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ); + int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ); + void simplify( FullModelChecker * mc, FirstOrderModelFmc * m ); + void debugPrint(const char * tr, Node op, FullModelChecker * m); +}; + + +class FullModelChecker : public QModelBuilder +{ +protected: + Node d_true; + Node d_false; + std::map<TypeNode, std::map< Node, int > > d_rep_ids; + std::map<Node, Def > d_quant_models; + std::map<Node, Node > d_quant_cond; + std::map< TypeNode, Node > d_array_cond; + std::map< Node, Node > d_array_term_cond; + std::map<Node, std::map< Node, int > > d_quant_var_id; + std::map<Node, std::vector< int > > d_star_insts; + void initializeType( FirstOrderModelFmc * fm, TypeNode tn ); + Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); + bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); +protected: + void makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, + std::map< int, std::map< int, Node > >& changed_vals ); + void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, + std::map< int, std::map< int, Node > >& changed_vals ); +private: + void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ); + + void doNegate( Def & dc ); + void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ); + void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v); + void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc ); + + void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, + Def & df, std::vector< Def > & dc, int index, + std::vector< Node > & cond, std::vector<Node> & val ); + void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, + std::map< int, Node > & entries, int index, + std::vector< Node > & cond, std::vector< Node > & val, + EntryTrie & curr); + + void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, + std::vector< Def > & dc, int index, + std::vector< Node > & cond, std::vector<Node> & val ); + int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); + Node doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk = true ); + bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); + Node mkCond( std::vector< Node > & cond ); + Node mkCondDefault( FirstOrderModelFmc * fm, Node f ); + void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ); + void mkCondVec( Node n, std::vector< Node > & cond ); + Node mkArrayCond( Node a ); + Node evaluateInterpreted( Node n, std::vector< Node > & vals ); + Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); +public: + FullModelChecker( context::Context* c, QuantifiersEngine* qe ); + ~FullModelChecker(){} + + bool optBuildAtFullModel(); + + int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; } + + void debugPrintCond(const char * tr, Node n, bool dispStar = false); + void debugPrint(const char * tr, Node n, bool dispStar = false); + + bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); + + Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); + + /** process build model */ + void processBuildModel(TheoryModel* m, bool fullModel); + /** get current model value */ + Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial ); + + bool useSimpleModels(); +}; + +} +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index e495b39c0..157861670 100644 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -29,10 +29,10 @@ using namespace CVC4::theory::quantifiers; InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ - Assert( n.hasAttribute(InstConstantAttribute()) ); + Assert( TermDb::hasInstConstAttr(n) ); int count = 0; for( size_t i=0; i<n.getNumChildren(); i++ ){ - if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){ + if( n[i].getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr(n[i]) ){ d_children.push_back( InstGenProcess( n[i] ) ); d_children_index.push_back( i ); d_children_map[ i ] = count; @@ -47,7 +47,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ d_match_values.push_back( val ); d_matches.push_back( InstMatch( &m ) ); - qe->getModelEngine()->getModelBuilder()->d_instGenMatches++; + ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->d_instGenMatches++; } } } @@ -92,7 +92,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto //for each term we consider, calculate a current match for( size_t i=0; i<considerTerms.size(); i++ ){ Node n = considerTerms[i]; - bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n ); bool hadSuccess CVC4_UNUSED = false; for( int t=(isSelected ? 0 : 1); t<2; t++ ){ if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ @@ -193,7 +193,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto //process all values for( size_t i=0; i<considerTerms.size(); i++ ){ Node n = considerTerms[i]; - bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n ); for( int t=(isSelected ? 0 : 1); t<2; t++ ){ //do not consider ground case if it is already congruent to another ground term if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index f6a0dad11..d55f72a88 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -134,18 +134,27 @@ Node InstMatch::getValue( Node var ) const{ } } +Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) { + return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) ); +} + void InstMatch::set(TNode var, TNode n){ Assert( !var.isNull() ); - if( !n.isNull() &&// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations - //var.getType() == n.getType() - !n.getType().isSubtypeOf( var.getType() ) ){ - Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl; - Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; - Assert(false); + if (Trace.isOn("inst-match-warn")) { + // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations + if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){ + Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl; + Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; + } } + Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) ); d_map[var] = n; } +void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) { + set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n ); +} + /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){ if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 127f83c60..72447fd66 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -92,8 +92,11 @@ public: void erase(Node node){ d_map.erase(node); } /** get */ Node get( TNode var ) { return d_map[var]; } + Node get( QuantifiersEngine* qe, Node f, int i ); /** set */ void set(TNode var, TNode n); + void set( QuantifiersEngine* qe, Node f, int i, TNode n ); + /** size */ size_t size(){ return d_map.size(); } /* iterator */ std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index de7f2f373..bf4bb15a6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -32,16 +32,16 @@ namespace inst { InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){ d_active_add = false; - Assert( pat.hasAttribute(InstConstantAttribute()) ); + Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); d_pattern = pat; d_match_pattern = pat; d_next = NULL; } -void InstMatchGenerator::setActiveAdd(){ - d_active_add = true; +void InstMatchGenerator::setActiveAdd(bool val){ + d_active_add = val; if( d_next!=NULL ){ - d_next->setActiveAdd(); + d_next->setActiveAdd(val); } } @@ -52,28 +52,43 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //we want to add the children of the NOT d_match_pattern = d_pattern[0]; } - if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){ - if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){ - Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) ); - //swap sides - Node pat = d_pattern; - d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); - d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern; - if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[1]; - }else{ - d_match_pattern = d_pattern[0][0]; + if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ + //make sure the matching portion of the equality is on the LHS of d_pattern + // and record what d_match_pattern is + if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || + d_match_pattern[0].getKind()==INST_CONSTANT ){ + if( d_match_pattern[1].getKind()!=INST_CONSTANT ){ + Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ); + Node mp = d_match_pattern[1]; + //swap sides + Node pat = d_pattern; + if(d_match_pattern.getKind()==GEQ){ + d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] ); + d_pattern = d_pattern.negate(); + }else{ + d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); + } + d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern; + d_match_pattern = mp; } - }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){ - Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) ); - if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[0]; + }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || + d_match_pattern[1].getKind()==INST_CONSTANT ){ + if( d_match_pattern[0].getKind()!=INST_CONSTANT ){ + Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ); + if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching + d_match_pattern = d_match_pattern[0]; + }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){ + d_match_pattern = d_match_pattern[0]; + } } } } + Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; + + //now, collect children of d_match_pattern int childMatchPolicy = MATCH_GEN_DEFAULT; for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy ); d_children.push_back( cimg ); @@ -83,10 +98,11 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat } } - Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; - //create candidate generator - if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + if( d_match_pattern.getKind()==INST_CONSTANT ){ + d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); + } + else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ @@ -96,50 +112,40 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //candidates will be all disequalities d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); } - }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){ + }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || + d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); if( d_pattern.getKind()==NOT ){ - Unimplemented("Disequal generator unimplemented"); + if (d_pattern[0][1].getKind()!=INST_CONSTANT) { + Unimplemented("Disequal generator unimplemented"); + }else{ + d_eq_class = d_pattern[0][1]; + } }else{ - Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); - //we are matching only in a particular equivalence class - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); //store the equivalence class that we will call d_cg->reset( ... ) on d_eq_class = d_pattern[1]; } + Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); + //we are matching only in a particular equivalence class + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ - //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ - //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; - //} //we will be scanning lists trying to find d_match_pattern.getOperator() d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); }else{ d_cg = new CandidateGeneratorQueue; - if( !Trigger::isArithmeticTrigger( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ - Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; - }else{ - Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl; - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; - } - //we will treat this as match gen internal arithmetic - d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC; - } + Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; + d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; } } } /** get match (not modulo equality) */ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){ - Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" - << m << ")" << ", " << d_children.size() << std::endl; + Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" + << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; Assert( !d_match_pattern.isNull() ); if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ return true; - }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){ - return getMatchArithmetic( t, m, qe ); }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ return false; }else{ @@ -149,12 +155,12 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi InstMatch prev( &m ); //if t is null Assert( !t.isNull() ); - Assert( !t.hasAttribute(InstConstantAttribute()) ); + Assert( !quantifiers::TermDb::hasInstConstAttr(t) ); Assert( t.getKind()==d_match_pattern.getKind() ); Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() ); //first, check if ground arguments are not equal, or a match is in conflict for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ Node vv = d_match_pattern[i]; Node tt = t[i]; @@ -164,24 +170,54 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } if( !m.setMatch( q, vv, tt ) ){ //match is in conflict - Debug("matching-debug") << "Match in conflict " << tt << " and " + Trace("matching-debug") << "Match in conflict " << tt << " and " << vv << " because " << m.get(vv) << std::endl; - Debug("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl; + Trace("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl; success = false; break; } } }else{ if( !q->areEqual( d_match_pattern[i], t[i] ) ){ - Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; + Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; //ground arguments are not equal success = false; break; } } } + //for relational matching + if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){ + //also must fit match to equivalence class + bool pol = d_pattern.getKind()!=NOT; + Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern; + Node t_match; + if( pol ){ + if (pat.getKind()==GT) { + Node r = NodeManager::currentNM()->mkConst( Rational(-1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else{ + t_match = t; + } + }else{ + if(pat.getKind()==EQUAL) { + Node r = NodeManager::currentNM()->mkConst( Rational(1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else if( pat.getKind()==IFF ){ + t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) ); + }else if( pat.getKind()==GEQ ){ + Node r = NodeManager::currentNM()->mkConst( Rational(1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else if( pat.getKind()==GT ){ + t_match = t; + } + } + if( !t_match.isNull() && !m.setMatch( q, d_eq_class, t_match ) ){ + success = false; + } + } if( success ){ //now, fit children into match //we will be requesting candidates for matching terms for each child @@ -208,95 +244,45 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } -bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){ - Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl; - if( !d_arith_coeffs.empty() ){ - NodeBuilder<> tb(kind::PLUS); - Node ic = Node::null(); - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << it->first << " -> " << it->second << std::endl; - if( !it->first.isNull() ){ - if( m.find( it->first )==m.end() ){ - //see if we can choose this to set - if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){ - ic = it->first; - } - }else{ - Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl; - Node tm = m.get( it->first ); - if( !it->second.isNull() ){ - tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm ); - } - tb << tm; - } - }else{ - tb << it->second; - } - } - if( !ic.isNull() ){ - Node tm; - if( tb.getNumChildren()==0 ){ - tm = t; - }else{ - tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; - tm = NodeManager::currentNM()->mkNode( MINUS, t, tm ); - } - if( !d_arith_coeffs[ ic ].isNull() ){ - Assert( !ic.getType().isInteger() ); - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() ); - tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm ); - } - m.set( ic, Rewriter::rewrite( tm )); - //set the rest to zeros - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - if( !it->first.isNull() ){ - if( m.find( it->first )==m.end() ){ - m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) ); - } - } - } - Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl; - return true; - }else{ - return false; - } - }else{ - return false; - } -} - - /** reset instantiation round */ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ - if( d_match_pattern.isNull() ){ - for( int i=0; i<(int)d_children.size(); i++ ){ - d_children[i]->resetInstantiationRound( qe ); - } - }else{ + if( !d_match_pattern.isNull() ){ + Trace("matching-debug2") << this << " reset instantiation round." << std::endl; + d_needsReset = true; if( d_cg ){ d_cg->resetInstantiationRound(); } } + if( d_next ){ + d_next->resetInstantiationRound( qe ); + } } void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ + Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl; if( !eqc.isNull() ){ d_eq_class = eqc; } //we have a specific equivalence class in mind //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term //just look in equivalence class of the RHS - d_cg->reset( d_eq_class ); + d_cg->reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class ); + d_needsReset = false; } bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ + if( d_needsReset ){ + Trace("matching") << "Reset not done yet, must do the reset..." << std::endl; + reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe ); + } m.d_matched = Node::null(); - //Debug("matching") << this << " " << d_pattern << " get next match 2 " << m << " in eq class " << d_eq_class << std::endl; + Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl; bool success = false; Node t; do{ //get the next candidate term t t = d_cg->getNextCandidate(); + Trace("matching-debug2") << "Matching candidate : " << t << std::endl; //if t not null, try to fit it into match m if( !t.isNull() && t.getType()==d_match_pattern.getType() ){ success = getMatch( f, t, m, qe ); @@ -304,9 +290,9 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* }while( !success && !t.isNull() ); m.d_matched = t; if( !success ){ - //Debug("matching") << this << " failed, reset " << d_eq_class << std::endl; + Trace("matching") << this << " failed, reset " << d_eq_class << std::endl; //we failed, must reset - reset( d_eq_class, qe ); + reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe ); } return success; } diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 4c954fa81..5d2128922 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -44,13 +44,14 @@ public: /** add ground term t, called when t is added to term db */ virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0; /** set active add */ - virtual void setActiveAdd() {} + virtual void setActiveAdd( bool val ) {} };/* class IMGenerator */ class CandidateGenerator; class InstMatchGenerator : public IMGenerator { private: + bool d_needsReset; /** candidate generator */ CandidateGenerator* d_cg; /** policy to use for matching */ @@ -72,12 +73,8 @@ public: MATCH_GEN_DEFAULT = 0, MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers //others (internally used) - MATCH_GEN_INTERNAL_ARITHMETIC, MATCH_GEN_INTERNAL_ERROR, }; -private: - /** for arithmetic */ - bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); public: /** get the match against ground term or formula t. d_match_pattern and t should have the same shape. @@ -108,7 +105,7 @@ public: int addTerm( Node f, Node t, QuantifiersEngine* qe ); bool d_active_add; - void setActiveAdd(); + void setActiveAdd( bool val ); static InstMatchGenerator* mkInstMatchGenerator( Node pat, QuantifiersEngine* qe ); static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe ); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index dbdf95613..4fe4072a3 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -41,6 +41,19 @@ bool InstStrategySimplex::calculateShouldProcess( Node f ){ return false; } +void getInstantiationConstants( Node n, std::vector< Node >& ics ){ + if( n.getKind()==INST_CONSTANT ){ + if( std::find( ics.begin(), ics.end(), n )==ics.end() ){ + ics.push_back( n ); + } + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + getInstantiationConstants( n[i], ics ); + } + } +} + + void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){ Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl; d_instRows.clear(); @@ -54,37 +67,69 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ArithVar x = *vi; if( d_th->d_internal->d_partialModel.hasEitherBound( x ) ){ Node n = avnm.asNode(x); - Node f; - NodeBuilder<> t(kind::PLUS); - if( n.getKind()==PLUS ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - addTermToRow( x, n[i], f, t ); + + //collect instantiation constants + std::vector< Node > ics; + getInstantiationConstants( n, ics ); + for( unsigned i=0; i<ics.size(); i++ ){ + + NodeBuilder<> t(kind::PLUS); + if( n.getKind()==PLUS ){ + for( int j=0; j<(int)n.getNumChildren(); j++ ){ + addTermToRow( ics[i], x, n[j], t ); + } + }else{ + addTermToRow( ics[i], x, n, t ); } - }else{ - addTermToRow( x, n, f, t ); - } - if( f!=Node::null() ){ - d_instRows[f].push_back( x ); + d_instRows[ics[i]].push_back( x ); //this theory has constraints from f + Node f = TermDb::getInstConstAttr(ics[i]); Debug("quant-arith") << "Has constraints from " << f << std::endl; //set that we should process it d_quantActive[ f ] = true; //set tableaux term if( t.getNumChildren()==0 ){ - d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) ); + d_tableaux_term[ics[i]][x] = NodeManager::currentNM()->mkConst( Rational(0) ); }else if( t.getNumChildren()==1 ){ - d_tableaux_term[x] = t.getChild( 0 ); + d_tableaux_term[ics[i]][x] = t.getChild( 0 ); }else{ - d_tableaux_term[x] = t; + d_tableaux_term[ics[i]][x] = t; } } } } //print debug + Debug("quant-arith-debug") << std::endl; debugPrint( "quant-arith-debug" ); d_counter++; } +void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){ + if( n.getKind()==MULT ){ + if( TermDb::hasInstConstAttr(n[1]) ){ + if( n[1]==i ){ + d_ceTableaux[i][x][ n[1] ] = n[0]; + }else{ + d_tableaux_ce_term[i][x][ n[1] ] = n[0]; + } + }else{ + d_tableaux[i][x][ n[1] ] = n[0]; + t << n; + } + }else{ + if( TermDb::hasInstConstAttr(n) ){ + if( n==i ){ + d_ceTableaux[i][x][ n ] = Node::null(); + }else{ + d_tableaux_ce_term[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); + } + }else{ + d_tableaux[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); + t << n; + } + } +} + int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ if( e<2 ){ return STATUS_UNFINISHED; @@ -92,48 +137,51 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ //Notice() << f << std::endl; //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl; //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl; - Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl; - for( int j=0; j<(int)d_instRows[f].size(); j++ ){ - ArithVar x = d_instRows[f][j]; - if( !d_ceTableaux[x].empty() ){ - Debug("quant-arith-simplex") << "Check row " << x << std::endl; - //instantiation row will be A*e + B*t = beta, - // where e is a vector of terms , and t is vector of ground terms. - // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant - // We will construct the term ( beta - B*t)/coeff to use for e_i. - InstMatch m; - //By default, choose the first instantiation constant to be e_i. - Node var = d_ceTableaux[x].begin()->first; - if( var.getType().isInteger() ){ - std::map< Node, Node >::iterator it = d_ceTableaux[x].begin(); - //try to find coefficent that is +/- 1 - while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){ - ++it; - if( it==d_ceTableaux[x].end() ){ - var = Node::null(); - }else{ - var = it->first; + for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); + Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; + for( int j=0; j<(int)d_instRows[ic].size(); j++ ){ + ArithVar x = d_instRows[ic][j]; + if( !d_ceTableaux[ic][x].empty() ){ + Debug("quant-arith-simplex") << "Check row " << ic << " " << x << std::endl; + //instantiation row will be A*e + B*t = beta, + // where e is a vector of terms , and t is vector of ground terms. + // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant + // We will construct the term ( beta - B*t)/coeff to use for e_i. + InstMatch m; + //By default, choose the first instantiation constant to be e_i. + Node var = d_ceTableaux[ic][x].begin()->first; + if( var.getType().isInteger() ){ + std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); + //try to find coefficent that is +/- 1 + while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){ + ++it; + if( it==d_ceTableaux[ic][x].end() ){ + var = Node::null(); + }else{ + var = it->first; + } } + //otherwise, try one that divides all ground term coefficients? DO_THIS } - //otherwise, try one that divides all ground term coefficients? DO_THIS - } - if( !var.isNull() ){ - Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; - doInstantiation( f, d_tableaux_term[x], x, m, var ); - }else{ - Debug("quant-arith-simplex") << "Could not find var." << std::endl; + if( !var.isNull() ){ + Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; + doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ); + }else{ + Debug("quant-arith-simplex") << "Could not find var." << std::endl; + } + ////choose a new variable based on alternation strategy + //int index = d_counter%(int)d_th->d_ceTableaux[x].size(); + //Node var; + //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){ + // if( index==0 ){ + // var = it->first; + // break; + // } + // index--; + //} + //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var ); } - ////choose a new variable based on alternation strategy - //int index = d_counter%(int)d_th->d_ceTableaux[x].size(); - //Node var; - //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){ - // if( index==0 ){ - // var = it->first; - // break; - // } - // index--; - //} - //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var ); } } } @@ -141,34 +189,6 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ } -void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){ - if( n.getKind()==MULT ){ - if( n[1].hasAttribute(InstConstantAttribute()) ){ - f = n[1].getAttribute(InstConstantAttribute()); - if( n[1].getKind()==INST_CONSTANT ){ - d_ceTableaux[x][ n[1] ] = n[0]; - }else{ - d_tableaux_ce_term[x][ n[1] ] = n[0]; - } - }else{ - d_tableaux[x][ n[1] ] = n[0]; - t << n; - } - }else{ - if( n.hasAttribute(InstConstantAttribute()) ){ - f = n.getAttribute(InstConstantAttribute()); - if( n.getKind()==INST_CONSTANT ){ - d_ceTableaux[x][ n ] = Node::null(); - }else{ - d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); - } - }else{ - d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); - t << n; - } - } -} - void InstStrategySimplex::debugPrint( const char* c ){ ArithVariables& avnm = d_th->d_internal->d_partialModel; ArithVariables::var_iterator vi, vend; @@ -218,14 +238,17 @@ void InstStrategySimplex::debugPrint( const char* c ){ Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); } Debug(c) << std::endl; - Debug(c) << " Instantiation rows: "; - for( int i=0; i<(int)d_instRows[f].size(); i++ ){ - if( i>0 ){ - Debug(c) << ", "; + for( int j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){ + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); + Debug(c) << " Instantiation rows for " << ic << " : "; + for( int i=0; i<(int)d_instRows[ic].size(); i++ ){ + if( i>0 ){ + Debug(c) << ", "; + } + Debug(c) << d_instRows[ic][i]; } - Debug(c) << d_instRows[f][i]; + Debug(c) << std::endl; } - Debug(c) << std::endl; } } @@ -234,15 +257,15 @@ void InstStrategySimplex::debugPrint( const char* c ){ // t[e] is a vector of terms containing instantiation constants from f, // and term is a ground term (c1*t1 + ... + cn*tn). // We construct the term ( beta - term )/coeff to use as an instantiation for var. -bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){ +bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){ //first try +delta - if( doInstantiation2( f, term, x, m, var ) ){ + if( doInstantiation2( f, ic, term, x, m, var ) ){ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith); return true; }else{ #ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA //otherwise try -delta - if( doInstantiation2( f, term, x, m, var, true ) ){ + if( doInstantiation2( f, ic, term, x, m, var, true ) ){ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus); return true; }else{ @@ -254,16 +277,16 @@ bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMa } } -bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ +bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ // make term ( beta - term )/coeff Node beta = getTableauxValue( x, minus_delta ); Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); - if( !d_ceTableaux[x][var].isNull() ){ + if( !d_ceTableaux[ic][x][var].isNull() ){ if( var.getType().isInteger() ){ - Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); - instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal ); + Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); + instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal ); }else{ - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() ); + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() ); instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); } } @@ -327,81 +350,9 @@ int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){ Node InstStrategyDatatypesValue::getValueFor( Node n ){ //simply get the ground value for n in the current model, if it exists, // or return an arbitrary ground term otherwise - if( !n.hasAttribute(InstConstantAttribute()) ){ + if( !TermDb::hasInstConstAttr(n) ){ return n; }else{ return n; } - /* FIXME - - Debug("quant-datatypes-debug") << "get value for " << n << std::endl; - if( !n.hasAttribute(InstConstantAttribute()) ){ - return n; - }else{ - Assert( n.getType().isDatatype() ); - //check if in equivalence class with ground term - Node rep = getRepresentative( n ); - Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl; - if( !rep.hasAttribute(InstConstantAttribute()) ){ - return rep; - }else{ - if( !n.getType().isDatatype() ){ - return n.getType().mkGroundTerm(); - }else{ - if( n.getKind()==APPLY_CONSTRUCTOR ){ - std::vector< Node > children; - children.push_back( n.getOperator() ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( getValueFor( n[i] ) ); - } - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - }else{ - const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); - TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels; - //otherwise, use which constructor the inst constant is current chosen to be - if( labels->find( n )!=labels->end() ){ - TheoryDatatypes::EqList* lbl = (*labels->find( n )).second; - int tIndex = -1; - if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){ - Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl; - tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr()); - }else{ - Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl; - //must find a possible choice - vector< bool > possibleCons; - possibleCons.resize( dt.getNumConstructors(), true ); - for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) { - Node leqn = (*j); - possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false; - } - for( unsigned int j=0; j<possibleCons.size(); j++ ) { - if( possibleCons[j] ){ - tIndex = j; - break; - } - } - } - Assert( tIndex!=-1 ); - Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() ); - Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl; - std::vector< Node > children; - children.push_back( cons ); - for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) { - Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n ); - if( n.hasAttribute(InstConstantAttribute()) ){ - InstConstantAttribute ica; - sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) ); - } - Node snn = getValueFor( sn ); - children.push_back( snn ); - } - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - }else{ - return n.getType().mkGroundTerm(); - } - } - } - } - } - */ } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index a45318489..821beeae0 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -49,19 +49,19 @@ private: /** for each quantifier, simplex rows */ std::map< Node, std::vector< arith::ArithVar > > d_instRows; /** tableaux */ - std::map< arith::ArithVar, Node > d_tableaux_term; - std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term; - std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux; + std::map< Node, std::map< arith::ArithVar, Node > > d_tableaux_term; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux_ce_term; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux; /** ce tableaux */ - std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux; /** get value */ Node getTableauxValue( Node n, bool minus_delta = false ); Node getTableauxValue( arith::ArithVar v, bool minus_delta = false ); /** do instantiation */ - bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var ); - bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); + bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var ); + bool doInstantiation2( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); /** add term to row */ - void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t ); + void addTermToRow( Node ic, arith::ArithVar x, Node n, NodeBuilder<>& t ); /** print debug */ void debugPrint( const char* c ); private: diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 0e1266e0d..ef81d55a1 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -144,7 +144,11 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) } if( gen ){ generateTriggers( f, effort, e, status ); + if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){ + Trace("no-trigger") << "Could not find trigger for " << f << std::endl; + } } + //if( e==4 ){ // d_processed_trigger.clear(); // d_quantEngine->getEqualityQuery()->setLiberal( true ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 77df69456..628f8b14a 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -92,7 +92,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ NodeBuilder<> nb(kind::OR); nb << f << ceLit; Node lem = nb; - Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; d_quantEngine->getOutputChannel().lemma( lem ); addedLemma = true; } @@ -197,7 +197,10 @@ void InstantiationEngine::check( Theory::Effort e ){ << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( options::cbqi() && hasAddedCbqiLemma( n ) ){ + //it is not active if we have found the skolemized negation is unsat + if( n.hasAttribute(QRewriteRuleAttribute()) ){ + d_quant_active[n] = false; + }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n ); bool active, value; bool ceValue = false; @@ -210,7 +213,9 @@ void InstantiationEngine::check( Theory::Effort e ){ d_quant_active[n] = active; if( active ){ Debug("quantifiers") << " Active : " << n; - quantActive = true; + if( !TermDb::hasInstConstAttr(n) ){ + quantActive = true; + } }else{ Debug("quantifiers") << " NOT active : " << n; if( d_quantEngine->getValuation().isDecision( cel ) ){ @@ -226,14 +231,18 @@ void InstantiationEngine::check( Theory::Effort e ){ Debug("quantifiers") << ", ce is asserted"; } Debug("quantifiers") << std::endl; + //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine }else{ d_quant_active[n] = true; - quantActive = true; + if( !TermDb::hasInstConstAttr(n) ){ + quantActive = true; + } Debug("quantifiers") << " Active : " << n << ", no ce assigned." << std::endl; } Debug("quantifiers-relevance") << "Quantifier : " << n << std::endl; Debug("quantifiers-relevance") << " Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl; Debug("quantifiers") << " Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl; + Trace("inst-engine-debug") << "Process : " << n << " " << d_quant_active[n] << std::endl; } if( quantActive ){ bool addedLemmas = doInstantiationRound( e ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 0b74cfc5e..5edf2de96 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -18,7 +18,6 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_model.h" #include "theory/uf/theory_uf_strong_solver.h" -#include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/model_builder.h" @@ -33,6 +32,65 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; + +QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) : +TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){ + d_considerAxioms = true; +} + +bool QModelBuilder::isQuantifierActive( Node f ) { + return !f.hasAttribute(QRewriteRuleAttribute()); +} + + +bool QModelBuilder::optUseModel() { + return options::fmfModelBasedInst(); +} + +void QModelBuilder::debugModel( FirstOrderModel* fm ){ + //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true + if( Trace.isOn("quant-model-warn") ){ + Trace("quant-model-warn") << "Testing quantifier instantiations..." << std::endl; + int tests = 0; + int bad = 0; + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + std::vector< Node > vars; + for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ + vars.push_back( f[0][j] ); + } + RepSetIterator riter( d_qe, &(fm->d_rep_set) ); + if( riter.setQuantifier( f ) ){ + while( !riter.isFinished() ){ + tests++; + std::vector< Node > terms; + for( int i=0; i<riter.getNumTerms(); i++ ){ + terms.push_back( riter.getTerm( i ) ); + } + Node n = d_qe->getInstantiation( f, vars, terms ); + Node val = fm->getValue( n ); + if( val!=fm->d_true ){ + Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; + Trace("quant-model-warn") << " " << f << std::endl; + Trace("quant-model-warn") << " Evaluates to " << val << std::endl; + bad++; + } + riter.increment(); + } + Trace("quant-model-warn") << "Tested " << tests << " instantiations"; + if( bad>0 ){ + Trace("quant-model-warn") << ", " << bad << " failed" << std::endl; + } + Trace("quant-model-warn") << "." << std::endl; + }else{ + Trace("quant-model-warn") << "Warning: Could not test quantifier " << f << std::endl; + } + } + } +} + + + bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ if( argIndex<(int)n.getNumChildren() ){ Node r; @@ -53,49 +111,25 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ } } -ModelEngineBuilder::ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ) : -TheoryEngineModelBuilder( qe->getTheoryEngine() ), -d_qe( qe ), d_curr_model( c, NULL ){ - d_considerAxioms = true; + +QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) : +QModelBuilder( c, qe ) { + } -void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){ - //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true - if( Trace.isOn("quant-model-warn") ){ - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - std::vector< Node > vars; - for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ - vars.push_back( f[0][j] ); - } - RepSetIterator riter( &(fm->d_rep_set) ); - riter.setQuantifier( f ); - while( !riter.isFinished() ){ - std::vector< Node > terms; - for( int i=0; i<riter.getNumTerms(); i++ ){ - terms.push_back( riter.getTerm( i ) ); - } - Node n = d_qe->getInstantiation( f, vars, terms ); - Node val = fm->getValue( n ); - if( val!=fm->d_true ){ - Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; - Trace("quant-model-warn") << " " << f << std::endl; - Trace("quant-model-warn") << " Evaluates to " << val << std::endl; - } - riter.increment(); - } - } - } +Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) { + return n; } -void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { - FirstOrderModel* fm = (FirstOrderModel*)m; +void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { + FirstOrderModel* f = (FirstOrderModel*)m; + FirstOrderModelIG* fm = f->asFirstOrderModelIG(); if( fullModel ){ Assert( d_curr_model==fm ); //update models for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ it->second.update( fm ); - Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl; + Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl; //construct function values fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" ); } @@ -106,7 +140,6 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { debugModel( fm ); }else{ d_curr_model = fm; - d_addedLemmas = 0; d_didInstGen = false; //reset the internal information reset( fm ); @@ -186,12 +219,13 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } } //construct the model if necessary - if( d_addedLemmas==0 || optExhInstNonInstGenQuant() ){ + if( d_addedLemmas==0 ){ //if no immediate exceptions, build the model // this model will be an approximation that will need to be tested via exhaustive instantiation Trace("model-engine-debug") << "Building model..." << std::endl; //build model for UF for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl; constructModelUf( fm, it->first ); } /* @@ -211,7 +245,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } } -int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){ +int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){ //create the basis match if necessary if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){ @@ -254,17 +288,18 @@ int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){ return 0; } -void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ +void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); d_uf_model_constructed.clear(); //determine if any functions are constant - for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){ Node op = it->first; TermArgBasisTrie tabt; - for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){ + Node n = fmig->d_uf_terms[op][i]; //for calculating if op is constant if( !n.getAttribute(NoMatchAttribute()) ){ - Node v = fm->getRepresentative( n ); + Node v = fmig->getRepresentative( n ); if( i==0 ){ d_uf_prefs[op].d_const_val = v; }else if( v!=d_uf_prefs[op].d_const_val ){ @@ -273,10 +308,10 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } //for calculating terms that we don't need to consider - if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ + if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ if( !n.getAttribute(BasisNoMatchAttribute()) ){ //need to consider if it is not congruent modulo model basis - if( !tabt.addTerm( fm, n ) ){ + if( !tabt.addTerm( fmig, n ) ){ BasisNoMatchAttribute bnma; n.setAttribute(bnma,true); } @@ -284,10 +319,10 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } if( !d_uf_prefs[op].d_const_val.isNull() ){ - fm->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); - fm->d_uf_model_gen[op].makeModel( fm, it->second ); + fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); + fmig->d_uf_model_gen[op].makeModel( fmig, it->second ); Debug("fmf-model-cons") << "Function " << op << " is the constant function "; - fm->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val ); + fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val ); Debug("fmf-model-cons") << std::endl; d_uf_model_constructed[op] = true; }else{ @@ -296,7 +331,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } -bool ModelEngineBuilder::hasConstantDefinition( Node n ){ +bool QModelBuilderIG::hasConstantDefinition( Node n ){ Node lit = n.getKind()==NOT ? n[0] : n; if( lit.getKind()==APPLY_UF ){ Node op = lit.getOperator(); @@ -307,60 +342,141 @@ bool ModelEngineBuilder::hasConstantDefinition( Node n ){ return false; } -bool ModelEngineBuilder::optUseModel() { - return options::fmfModelBasedInst(); -} - -bool ModelEngineBuilder::optInstGen(){ +bool QModelBuilderIG::optInstGen(){ return options::fmfInstGen(); } -bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ +bool QModelBuilderIG::optOneQuantPerRoundInstGen(){ return options::fmfInstGenOneQuantPerRound(); } -bool ModelEngineBuilder::optExhInstNonInstGenQuant(){ - return options::fmfNewInstGen(); -} - -void ModelEngineBuilder::setEffort( int effort ){ - d_considerAxioms = effort>=1; -} - -ModelEngineBuilder::Statistics::Statistics(): - d_num_quants_init("ModelEngineBuilder::Number_Quantifiers", 0), - d_num_partial_quants_init("ModelEngineBuilder::Number_Partial_Quantifiers", 0), - d_init_inst_gen_lemmas("ModelEngineBuilder::Initialize_Inst_Gen_Lemmas", 0 ), - d_inst_gen_lemmas("ModelEngineBuilder::Inst_Gen_Lemmas", 0 ) +QModelBuilderIG::Statistics::Statistics(): + d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), + d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0), + d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ), + d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ), + d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ), + d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ), + d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ), + d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 ) { StatisticsRegistry::registerStat(&d_num_quants_init); StatisticsRegistry::registerStat(&d_num_partial_quants_init); StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas); StatisticsRegistry::registerStat(&d_inst_gen_lemmas); + StatisticsRegistry::registerStat(&d_eval_formulas); + StatisticsRegistry::registerStat(&d_eval_uf_terms); + StatisticsRegistry::registerStat(&d_eval_lits); + StatisticsRegistry::registerStat(&d_eval_lits_unknown); } -ModelEngineBuilder::Statistics::~Statistics(){ +QModelBuilderIG::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_num_quants_init); StatisticsRegistry::unregisterStat(&d_num_partial_quants_init); StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas); StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas); + StatisticsRegistry::unregisterStat(&d_eval_formulas); + StatisticsRegistry::unregisterStat(&d_eval_uf_terms); + StatisticsRegistry::unregisterStat(&d_eval_lits); + StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); } -bool ModelEngineBuilder::isQuantifierActive( Node f ){ - return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); +bool QModelBuilderIG::isQuantifierActive( Node f ){ + return !f.hasAttribute(QRewriteRuleAttribute()) && + ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); } -bool ModelEngineBuilder::isTermActive( Node n ){ +bool QModelBuilderIG::isTermActive( Node n ){ return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term - ( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments + ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments //and is not congruent modulo model basis //to another active term } +//do exhaustive instantiation +bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { + if( optUseModel() ){ + + RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) ); + if( riter.setQuantifier( f ) ){ + FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel(); + Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; + fmig->resetEvaluate(); + Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; + while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ + d_triedLemmas++; + for( int i=0; i<(int)riter.d_index.size(); i++ ){ + Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl; + } + int eval = 0; + int depIndex; + //see if instantiation is already true in current model + Debug("fmf-model-eval") << "Evaluating "; + riter.debugPrintSmall("fmf-model-eval"); + Debug("fmf-model-eval") << "Done calculating terms." << std::endl; + //if evaluate(...)==1, then the instantiation is already true in the model + // depIndex is the index of the least significant variable that this evaluation relies upon + depIndex = riter.getNumTerms()-1; + eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); + if( eval==1 ){ + Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; + }else{ + Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + } + if( eval==1 ){ + //instantiation is already true -> skip + riter.increment2( depIndex ); + }else{ + //instantiation was not shown to be true, construct the match + InstMatch m; + for( int i=0; i<riter.getNumTerms(); i++ ){ + m.set( d_qe, f, riter.d_index_order[i], riter.getTerm( i ) ); + } + Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; + //add as instantiation + if( d_qe->addInstantiation( f, m ) ){ + d_addedLemmas++; + //if the instantiation is show to be false, and we wish to skip multiple instantiations at once + if( eval==-1 ){ + riter.increment2( depIndex ); + }else{ + riter.increment(); + } + }else{ + Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + riter.increment(); + } + } + } + //print debugging information + if( fmig ){ + d_statistics.d_eval_formulas += fmig->d_eval_formulas; + d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms; + d_statistics.d_eval_lits += fmig->d_eval_lits; + d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown; + } + Trace("inst-fmf-ei") << "Finished: " << std::endl; + Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl; + Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl; + if( d_addedLemmas>1000 ){ + Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; + Trace("model-engine-warn") << " Inst Tried: " << d_triedLemmas << std::endl; + Trace("model-engine-warn") << " Inst Added: " << d_addedLemmas << std::endl; + Trace("model-engine-warn") << std::endl; + } + } + //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round + d_incomplete_check = riter.d_incomplete; + return true; + }else{ + return false; + } +} + -void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){ +void QModelBuilderDefault::reset( FirstOrderModel* fm ){ d_quant_selection_lit.clear(); d_quant_selection_lit_candidates.clear(); d_quant_selection_lit_terms.clear(); @@ -369,7 +485,7 @@ void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){ } -int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { +int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { /* size_t maxChildren = 0; for( size_t i=0; i<uf_terms.size(); i++ ){ @@ -383,7 +499,8 @@ int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms return 0; } -void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ +void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; //the pro/con preferences for this quantifier std::vector< Node > pro_con[2]; @@ -408,7 +525,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) // constant definitions. bool isConst = true; std::vector< Node > uf_terms; - if( n.hasAttribute(InstConstantAttribute()) ){ + if( TermDb::hasInstConstAttr(n) ){ isConst = false; if( gn.getKind()==APPLY_UF ){ uf_terms.push_back( gn ); @@ -416,9 +533,9 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) }else if( gn.getKind()==EQUAL ){ isConst = true; for( int j=0; j<2; j++ ){ - if( n[j].hasAttribute(InstConstantAttribute()) ){ + if( TermDb::hasInstConstAttr(n[j]) ){ if( n[j].getKind()==APPLY_UF && - fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){ + fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){ uf_terms.push_back( gn[j] ); isConst = isConst && hasConstantDefinition( gn[j] ); }else{ @@ -506,14 +623,14 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) for( int k=0; k<2; k++ ){ for( int j=0; j<(int)pro_con[k].size(); j++ ){ Node op = pro_con[k][j].getOperator(); - Node r = fm->getRepresentative( pro_con[k][j] ); + Node r = fmig->getRepresentative( pro_con[k][j] ); d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); } } } } -int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ +int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ int addedLemmas = 0; //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, @@ -523,17 +640,16 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){ bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT; Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i]; - Assert( lit.hasAttribute(InstConstantAttribute()) ); + Assert( TermDb::hasInstConstAttr(lit) ); std::vector< Node > tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); - d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f ); tr_terms.push_back( eq ); }else if( lit.getKind()==EQUAL ){ //collect trigger terms for( int j=0; j<2; j++ ){ - if( lit[j].hasAttribute(InstConstantAttribute()) ){ + if( TermDb::hasInstConstAttr(lit[j]) ){ if( lit[j].getKind()==APPLY_UF ){ tr_terms.push_back( lit[j] ); }else{ @@ -564,7 +680,8 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ return addedLemmas; } -void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ +void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); if( optReconsiderFuncConstants() ){ //reconsider constant functions that weren't necessary if( d_uf_model_constructed[op] ){ @@ -573,8 +690,8 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) Node v = d_uf_prefs[op].d_const_val; if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){ Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl; - fm->d_uf_model_tree[op].clear(); - fm->d_uf_model_gen[op].clear(); + fmig->d_uf_model_tree[op].clear(); + fmig->d_uf_model_gen[op].clear(); d_uf_model_constructed[op] = false; } } @@ -586,20 +703,20 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; //set the values in the model - for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){ + Node n = fmig->d_uf_terms[op][i]; if( isTermActive( n ) ){ - Node v = fm->getRepresentative( n ); - Trace("fmf-model-cons") << "Set term " << n << " : " << fm->d_rep_set.getIndexFor( v ) << " " << v << std::endl; + Node v = fmig->getRepresentative( n ); + Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl; //if this assertion did not help the model, just consider it ground //set n = v in the model tree //set it as ground value - fm->d_uf_model_gen[op].setValue( fm, n, v ); - if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){ + fmig->d_uf_model_gen[op].setValue( fm, n, v ); + if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){ //also set as default value if necessary - if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){ + if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){ Trace("fmf-model-cons") << " Set as default." << std::endl; - fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); if( n==defaultTerm ){ //incidentally already set, we will not need to find a default value setDefaultVal = false; @@ -607,7 +724,7 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) } }else{ if( n==defaultTerm ){ - fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); //incidentally already set, we will not need to find a default value setDefaultVal = false; } @@ -619,12 +736,19 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) Trace("fmf-model-cons") << " Choose default value..." << std::endl; //chose defaultVal based on heuristic, currently the best ratio of "pro" responses Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); + if( defaultVal.isNull() ){ + if (!fmig->d_rep_set.hasType(defaultTerm.getType())) { + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType()); + fmig->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt); + } + defaultVal = fmig->d_rep_set.d_type_reps[defaultTerm.getType()][0]; + } Assert( !defaultVal.isNull() ); - Trace("fmf-model-cons") << "Set default term : " << fm->d_rep_set.getIndexFor( defaultVal ) << std::endl; - fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); + Trace("fmf-model-cons") << "Set default term : " << fmig->d_rep_set.getIndexFor( defaultVal ) << std::endl; + fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); } Debug("fmf-model-cons") << " Making model..."; - fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] ); + fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] ); d_uf_model_constructed[op] = true; Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; } @@ -635,7 +759,7 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) ////////////////////// Inst-Gen style Model Builder /////////// -void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){ +void QModelBuilderInstGen::reset( FirstOrderModel* fm ){ //for new inst gen d_quant_selection_formula.clear(); d_term_selected.clear(); @@ -643,15 +767,15 @@ void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){ //d_sub_quant_inst_trie.clear();//* } -int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){ - int addedLemmas = ModelEngineBuilder::initializeQuantifier( f, fp ); +int QModelBuilderInstGen::initializeQuantifier( Node f, Node fp ){ + int addedLemmas = QModelBuilderIG::initializeQuantifier( f, fp ); for( size_t i=0; i<d_sub_quants[f].size(); i++ ){ addedLemmas += initializeQuantifier( d_sub_quants[f][i], fp ); } return addedLemmas; } -void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ +void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ //Node fp = getParentQuantifier( f );//* //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ); //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//* @@ -662,7 +786,6 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ) //if( !s.isNull() ){ // s = Rewriter::rewrite( s ); //} - d_qe->getTermDatabase()->setInstantiationConstantAttr( s, f ); Trace("sel-form-debug") << "Selection formula " << f << std::endl; Trace("sel-form-debug") << " " << s << std::endl; if( !s.isNull() ){ @@ -685,7 +808,7 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ) } -int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ +int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ int addedLemmas = 0; if( d_quant_sat.find( f )==d_quant_sat.end() ){ Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; @@ -802,7 +925,7 @@ Node mkAndSelectionFormula( Node n1, Node n2 ){ //if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context, // and NULL otherwise -Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){ +Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){ Trace("sel-form-debug") << "Looking for selection formula " << n << " " << polarity << std::endl; Node ret; if( n.getKind()==NOT ){ @@ -911,7 +1034,7 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar return ret; } -int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){ +int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){ if( fn.getType().isBoolean() ){ if( fn.getKind()==APPLY_UF ){ Node op = fn.getOperator(); @@ -929,13 +1052,13 @@ int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){ } } -void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){ +void QModelBuilderInstGen::setSelectedTerms( Node s ){ //if it is apply uf and has model basis arguments, then mark term as being "selected" if( s.getKind()==APPLY_UF ){ Assert( s.hasAttribute(ModelBasisArgAttribute()) ); if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl; - if( s.getAttribute(ModelBasisArgAttribute())==1 ){ + if( s.getAttribute(ModelBasisArgAttribute())!=0 ){ d_term_selected[ s ] = true; Trace("sel-form-term") << " " << s << " is a selected term." << std::endl; } @@ -945,7 +1068,7 @@ void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){ } } -bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){ +bool QModelBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){ if( n.getKind()==FORALL ){ return false; }else if( n.getKind()!=APPLY_UF ){ @@ -964,7 +1087,7 @@ bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption return true; } -void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){ +void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){ if( f!=fp ){ //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl; //std::cout << " " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl; @@ -988,20 +1111,21 @@ void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp } } -void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ +void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); bool setDefaultVal = true; Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); //set the values in the model - for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){ + Node n = fmig->d_uf_terms[op][i]; if( isTermActive( n ) ){ - Node v = fm->getRepresentative( n ); - fm->d_uf_model_gen[op].setValue( fm, n, v ); + Node v = fmig->getRepresentative( n ); + fmig->d_uf_model_gen[op].setValue( fm, n, v ); } //also possible set as default if( d_term_selected.find( n )!=d_term_selected.end() || n==defaultTerm ){ - Node v = fm->getRepresentative( n ); - fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + Node v = fmig->getRepresentative( n ); + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); if( n==defaultTerm ){ setDefaultVal = false; } @@ -1010,12 +1134,12 @@ void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ) //set the overall default value if not set already (is this necessary??) if( setDefaultVal ){ Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); - fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); + fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); } - fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] ); + fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] ); d_uf_model_constructed[op] = true; } -bool ModelEngineBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ +bool QModelBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true ); -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 31448acee..b96c58767 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -25,6 +25,42 @@ namespace CVC4 { namespace theory { namespace quantifiers { + +class QModelBuilder : public TheoryEngineModelBuilder +{ +protected: + //the model we are working with + context::CDO< FirstOrderModel* > d_curr_model; + //quantifiers engine + QuantifiersEngine* d_qe; +public: + QModelBuilder( context::Context* c, QuantifiersEngine* qe ); + virtual ~QModelBuilder(){} + // is quantifier active? + virtual bool isQuantifierActive( Node f ); + //do exhaustive instantiation + virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } + //whether to construct model + virtual bool optUseModel(); + //whether to construct model at fullModel = true + virtual bool optBuildAtFullModel() { return false; } + //consider axioms + bool d_considerAxioms; + /** number of lemmas generated while building model */ + //is the exhaustive instantiation incomplete? + bool d_incomplete_check; + int d_addedLemmas; + int d_triedLemmas; + /** exist instantiation ? */ + virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } + //debug model + void debugModel( FirstOrderModel* fm ); +}; + + + + + /** Attribute true for nodes that should not be used when considered for inst-gen basis */ struct BasisNoMatchAttributeId {}; /** use the special for boolean flag */ @@ -47,17 +83,13 @@ public: /** model builder class * This class is capable of building candidate models based on the current quantified formulas * that are asserted. Use: - * (1) call ModelEngineBuilder::buildModel( m, false );, where m is a FirstOrderModel + * (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel * (2) if candidate model is determined to be a real model, - then call ModelEngineBuilder::buildModel( m, true ); + then call QModelBuilder::buildModel( m, true ); */ -class ModelEngineBuilder : public TheoryEngineModelBuilder +class QModelBuilderIG : public QModelBuilder { protected: - //quantifiers engine - QuantifiersEngine* d_qe; - //the model we are working with - context::CDO< FirstOrderModel* > d_curr_model; //map from operators to model preference data std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; //built model uf @@ -66,6 +98,8 @@ protected: bool d_didInstGen; /** process build model */ virtual void processBuildModel( TheoryModel* m, bool fullModel ); + /** get current model value */ + Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ); protected: //reset virtual void reset( FirstOrderModel* fm ) = 0; @@ -90,25 +124,13 @@ protected: //helper functions /** term has constant definition */ bool hasConstantDefinition( Node n ); public: - ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ); - virtual ~ModelEngineBuilder(){} - /** number of lemmas generated while building model */ - int d_addedLemmas; - //consider axioms - bool d_considerAxioms; - // set effort - void setEffort( int effort ); - //debug model - void debugModel( FirstOrderModel* fm ); + QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); + virtual ~QModelBuilderIG(){} public: - //whether to construct model - virtual bool optUseModel(); //whether to add inst-gen lemmas virtual bool optInstGen(); //whether to only consider only quantifier per round of inst-gen virtual bool optOneQuantPerRoundInstGen(); - //whether we should exhaustively instantiate quantifiers where inst-gen is not working - virtual bool optExhInstNonInstGenQuant(); /** statistics class */ class Statistics { public: @@ -116,22 +138,26 @@ public: IntStat d_num_partial_quants_init; IntStat d_init_inst_gen_lemmas; IntStat d_inst_gen_lemmas; + IntStat d_eval_formulas; + IntStat d_eval_uf_terms; + IntStat d_eval_lits; + IntStat d_eval_lits_unknown; Statistics(); ~Statistics(); }; Statistics d_statistics; - // is quantifier active? - bool isQuantifierActive( Node f ); // is term active bool isTermActive( Node n ); // is term selected virtual bool isTermSelected( Node n ) { return false; } - /** exist instantiation ? */ - virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } /** quantifier has inst-gen definition */ virtual bool hasInstGen( Node f ) = 0; /** did inst gen this round? */ bool didInstGen() { return d_didInstGen; } + // is quantifier active? + bool isQuantifierActive( Node f ); + //do exhaustive instantiation + bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); //temporary stats int d_numQuantSat; @@ -140,10 +166,10 @@ public: int d_numQuantNoSelForm; //temporary stat int d_instGenMatches; -};/* class ModelEngineBuilder */ +};/* class QModelBuilder */ -class ModelEngineBuilderDefault : public ModelEngineBuilder +class QModelBuilderDefault : public QModelBuilderIG { private: ///information for (old) InstGen //map from quantifiers to their selection literals @@ -167,15 +193,15 @@ protected: //theory-specific build models void constructModelUf( FirstOrderModel* fm, Node op ); public: - ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} - ~ModelEngineBuilderDefault(){} + QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} + ~QModelBuilderDefault(){} //options bool optReconsiderFuncConstants() { return true; } //has inst gen bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); } }; -class ModelEngineBuilderInstGen : public ModelEngineBuilder +class QModelBuilderInstGen : public QModelBuilderIG { private: ///information for (new) InstGen //map from quantifiers to their selection formulas @@ -217,8 +243,8 @@ private: //get parent quantifier Node getParentQuantifier( Node f ) { return d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; } public: - ModelEngineBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} - ~ModelEngineBuilderInstGen(){} + QModelBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} + ~QModelBuilderInstGen(){} // is term selected bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); } /** exist instantiation ? */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index a69b278c0..cb8cb8154 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -18,13 +18,10 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/quantifiers/options.h" -#include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" -#define EVAL_FAIL_SKIP_MULTIPLE - using namespace std; using namespace CVC4; using namespace CVC4::kind; @@ -35,15 +32,21 @@ using namespace CVC4::theory::inst; //Model Engine constructor ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : -QuantifiersModule( qe ), -d_rel_domain( qe, qe->getModel() ){ +QuantifiersModule( qe ){ - if( options::fmfNewInstGen() ){ - d_builder = new ModelEngineBuilderInstGen( c, qe ); + if( options::fmfFullModelCheck() ){ + d_builder = new fmcheck::FullModelChecker( c, qe ); + }else if( options::fmfNewInstGen() ){ + d_builder = new QModelBuilderInstGen( c, qe ); }else{ - d_builder = new ModelEngineBuilderDefault( c, qe ); + d_builder = new QModelBuilderDefault( c, qe ); } + if( options::fmfRelevantDomain() ){ + d_rel_dom = new RelevantDomain( qe, qe->getModel() ); + }else{ + d_rel_dom = NULL; + } } void ModelEngine::check( Theory::Effort e ){ @@ -57,6 +60,7 @@ void ModelEngine::check( Theory::Effort e ){ clSet = double(clock())/double(CLOCKS_PER_SEC); } ++(d_statistics.d_inst_rounds); + bool buildAtFullModel = d_builder->optBuildAtFullModel(); //two effort levels: first try exhaustive instantiation without axioms, then with. int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; for( int effort=startEffort; effort<2; effort++ ){ @@ -66,8 +70,9 @@ void ModelEngine::check( Theory::Effort e ){ Trace("model-engine") << "---Model Engine Round---" << std::endl; //initialize the model Trace("model-engine-debug") << "Build model..." << std::endl; - d_builder->setEffort( effort ); - d_builder->buildModel( fm, false ); + d_builder->d_considerAxioms = effort>=1; + d_builder->d_addedLemmas = 0; + d_builder->buildModel( fm, buildAtFullModel ); addedLemmas += (int)d_builder->d_addedLemmas; //if builder has lemmas, add and return if( addedLemmas==0 ){ @@ -81,11 +86,7 @@ void ModelEngine::check( Theory::Effort e ){ Debug("fmf-model-complete") << std::endl; debugPrint("fmf-model-complete"); //successfully built an acceptable model, now check it - addedLemmas += checkModel( check_model_full ); - }else if( d_builder->didInstGen() && d_builder->optExhInstNonInstGenQuant() ){ - Trace("model-engine-debug") << "Check model for non-inst gen quantifiers..." << std::endl; - //check quantifiers that inst-gen didn't apply to - addedLemmas += checkModel( check_model_no_inst_gen ); + addedLemmas += checkModel(); } } if( addedLemmas==0 ){ @@ -108,7 +109,7 @@ void ModelEngine::check( Theory::Effort e ){ //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - if( options::produceModels() ){ + if( options::produceModels() && !buildAtFullModel ){ // finish building the model d_builder->buildModel( fm, true ); } @@ -131,28 +132,12 @@ void ModelEngine::assertNode( Node f ){ } -bool ModelEngine::optOneInstPerQuantRound(){ - return options::fmfOneInstPerRound(); -} - -bool ModelEngine::optUseRelevantDomain(){ - return options::fmfRelevantDomain(); -} - bool ModelEngine::optOneQuantPerRound(){ return options::fmfOneQuantPerRound(); } -bool ModelEngine::optExhInstEvalSkipMultiple(){ -#ifdef EVAL_FAIL_SKIP_MULTIPLE - return true; -#else - return false; -#endif -} -int ModelEngine::checkModel( int checkOption ){ - int addedLemmas = 0; +int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); //for debugging if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){ @@ -161,27 +146,28 @@ int ModelEngine::checkModel( int checkOption ){ if( it->first.isSort() ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; Trace("model-engine-debug") << " "; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); for( size_t i=0; i<it->second.size(); i++ ){ //Trace("model-engine-debug") << it->second[i] << " "; Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl; } } } - //compute the relevant domain if necessary - if( optUseRelevantDomain() ){ - d_rel_domain.compute(); + //relevant domain? + if( d_rel_dom ){ + d_rel_dom->compute(); } + d_triedLemmas = 0; - d_testLemmas = 0; - d_relevantLemmas = 0; + d_addedLemmas = 0; d_totalLemmas = 0; - Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; + //for statistics for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - //keep track of total instantiations for statistics int totalInst = 1; for( size_t i=0; i<f[0].getNumChildren(); i++ ){ TypeNode tn = f[0][i].getType(); @@ -190,133 +176,85 @@ int ModelEngine::checkModel( int checkOption ){ } } d_totalLemmas += totalInst; - //determine if we should check this quantifiers - bool checkQuant = false; - if( checkOption==check_model_full ){ - checkQuant = d_builder->isQuantifierActive( f ); - }else if( checkOption==check_model_no_inst_gen ){ - checkQuant = !d_builder->hasInstGen( f ); - } - //if we need to consider this quantifier on this iteration - if( checkQuant ){ - addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); - if( Trace.isOn("model-engine-warn") ){ - if( addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); + } + + Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; + int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1; + for( int e=0; e<e_max; e++) { + if (d_addedLemmas==0) { + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + //determine if we should check this quantifier + if( d_builder->isQuantifierActive( f ) ){ + exhaustiveInstantiate( f, e ); + if( Trace.isOn("model-engine-warn") ){ + if( d_addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); + } + } + if( optOneQuantPerRound() && d_addedLemmas>0 ){ + break; + } } } - if( optOneQuantPerRound() && addedLemmas>0 ){ - break; - } } } //print debug information if( Trace.isOn("model-engine") ){ Trace("model-engine") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl; - Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; - Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; + Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_totalLemmas << std::endl; } - d_statistics.d_exh_inst_lemmas += addedLemmas; - return addedLemmas; + d_statistics.d_exh_inst_lemmas += d_addedLemmas; + return d_addedLemmas; } -int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ - int addedLemmas = 0; - Trace("inst-fmf-ei") << "Exhaustive instantiate " << 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->getTermDatabase()->getInstantiationConstant( f, i ) << " "; - } - Debug("inst-fmf-ei") << std::endl; - - //create a rep set iterator and iterate over the (relevant) domain of the quantifier - RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); - if( riter.setQuantifier( f ) ){ - //set the domain for the iterator (the sufficient set of instantiations to try) - if( useRelInstDomain ){ - riter.setDomain( d_rel_domain.d_quant_inst_domain[f] ); +void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ + //first check if the builder can do the exhaustive instantiation + d_builder->d_triedLemmas = 0; + d_builder->d_addedLemmas = 0; + d_builder->d_incomplete_check = false; + if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ + d_triedLemmas += d_builder->d_triedLemmas; + d_addedLemmas += d_builder->d_addedLemmas; + d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check; + }else{ + Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; + Debug("inst-fmf-ei") << " Instantiation Constants: "; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; } - d_quantEngine->getModel()->resetEvaluate(); - int tests = 0; - int triedLemmas = 0; - while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ - d_testLemmas++; - int eval = 0; - int depIndex; - if( d_builder->optUseModel() ){ - //see if instantiation is already true in current model - Debug("fmf-model-eval") << "Evaluating "; - riter.debugPrintSmall("fmf-model-eval"); - Debug("fmf-model-eval") << "Done calculating terms." << std::endl; - tests++; - //if evaluate(...)==1, then the instantiation is already true in the model - // depIndex is the index of the least significant variable that this evaluation relies upon - depIndex = riter.getNumTerms()-1; - eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); - if( eval==1 ){ - Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; - }else{ - Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; - } - } - if( eval==1 ){ - //instantiation is already true -> skip - riter.increment2( depIndex ); - }else{ + Debug("inst-fmf-ei") << std::endl; + //create a rep set iterator and iterate over the (relevant) domain of the quantifier + RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); + if( riter.setQuantifier( f ) ){ + Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; + int triedLemmas = 0; + int addedLemmas = 0; + while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m; for( int i=0; i<riter.getNumTerms(); i++ ){ - m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) ); + m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) ); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; - d_triedLemmas++; //add as instantiation if( d_quantEngine->addInstantiation( f, m ) ){ addedLemmas++; - //if the instantiation is show to be false, and we wish to skip multiple instantiations at once - if( eval==-1 && optExhInstEvalSkipMultiple() ){ - riter.increment2( depIndex ); - }else{ - riter.increment(); - } }else{ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; - riter.increment(); } + riter.increment(); } + d_addedLemmas += addedLemmas; + d_triedLemmas += triedLemmas; } - //print debugging information - d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas; - d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms; - d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits; - d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown; - int relevantInst = 1; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - relevantInst = relevantInst * (int)riter.d_domain[i].size(); - } - d_relevantLemmas += relevantInst; - Trace("inst-fmf-ei") << "Finished: " << std::endl; - //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; - Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; - Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; - Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; - Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl; - if( addedLemmas>1000 ){ - Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; - //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl; - Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl; - Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl; - Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl; - Trace("model-engine-warn") << " # Tests: " << tests << std::endl; - Trace("model-engine-warn") << std::endl; - } + //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round + d_incomplete_check = d_incomplete_check || riter.d_incomplete; } - //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = d_incomplete_check || riter.d_incomplete; - return addedLemmas; } void ModelEngine::debugPrint( const char* c ){ @@ -336,26 +274,14 @@ void ModelEngine::debugPrint( const char* c ){ ModelEngine::Statistics::Statistics(): d_inst_rounds("ModelEngine::Inst_Rounds", 0), - d_eval_formulas("ModelEngine::Eval_Formulas", 0 ), - d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ), - d_eval_lits("ModelEngine::Eval_Lits", 0 ), - d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ), d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); - StatisticsRegistry::registerStat(&d_eval_formulas); - StatisticsRegistry::registerStat(&d_eval_uf_terms); - StatisticsRegistry::registerStat(&d_eval_lits); - StatisticsRegistry::registerStat(&d_eval_lits_unknown); StatisticsRegistry::registerStat(&d_exh_inst_lemmas); } ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_inst_rounds); - StatisticsRegistry::unregisterStat(&d_eval_formulas); - StatisticsRegistry::unregisterStat(&d_eval_uf_terms); - StatisticsRegistry::unregisterStat(&d_eval_lits); - StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 386864164..1c2c38c51 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -20,6 +20,7 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/model_builder.h" #include "theory/model.h" +#include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/relevant_domain.h" namespace CVC4 { @@ -31,38 +32,31 @@ class ModelEngine : public QuantifiersModule friend class RepSetIterator; private: /** builder class */ - ModelEngineBuilder* d_builder; + QModelBuilder* d_builder; private: //analysis of current model: - //relevant domain - RelevantDomain d_rel_domain; - //is the exhaustive instantiation incomplete? - bool d_incomplete_check; + RelevantDomain* d_rel_dom; private: //options - bool optOneInstPerQuantRound(); - bool optUseRelevantDomain(); bool optOneQuantPerRound(); - bool optExhInstEvalSkipMultiple(); private: - enum{ - check_model_full, - check_model_no_inst_gen, - }; //check model - int checkModel( int checkOption ); - //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced - int exhaustiveInstantiate( Node f, bool useRelInstDomain = false ); + int checkModel(); + //exhaustively instantiate quantifier (possibly using mbqi) + void exhaustiveInstantiate( Node f, int effort = 0 ); private: //temporary statistics + //is the exhaustive instantiation incomplete? + bool d_incomplete_check; + int d_addedLemmas; int d_triedLemmas; - int d_testLemmas; int d_totalLemmas; - int d_relevantLemmas; public: ModelEngine( context::Context* c, QuantifiersEngine* qe ); ~ModelEngine(){} + //get relevant domain + RelevantDomain * getRelevantDomain() { return d_rel_dom; } //get the builder - ModelEngineBuilder* getModelBuilder() { return d_builder; } + QModelBuilder* getModelBuilder() { return d_builder; } public: void check( Theory::Effort e ); void registerQuantifier( Node f ); @@ -74,10 +68,6 @@ public: class Statistics { public: IntStat d_inst_rounds; - IntStat d_eval_formulas; - IntStat d_eval_uf_terms; - IntStat d_eval_lits; - IntStat d_eval_lits_unknown; IntStat d_exh_inst_lemmas; Statistics(); ~Statistics(); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 60f5a171d..57211ade7 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -24,8 +24,11 @@ option prenexQuant /--disable-prenex-quant bool :default true # Whether to variable-eliminate quantifiers. # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to # forall y. P( c, y ) -option varElimQuant --var-elim-quant bool :default false - enable variable elimination of quantified formulas +option varElimQuant /--disable-var-elim-quant bool :default true + disable simple variable elimination for quantified formulas + +option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true + disable simple ite lifting for quantified formulas # Whether to CNF quantifier bodies option cnfQuant --cnf-quant bool :default false @@ -47,6 +50,9 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false # Whether to perform quantifier macro expansion option macrosQuant --macros-quant bool :default false perform quantifiers macro expansions +# Whether to perform first-order propagation +option foPropQuant --fo-prop-quant bool :default false + perform first-order propagation on quantifiers # Whether to use smart triggers option smartTriggers /--disable-smart-triggers bool :default true @@ -54,6 +60,8 @@ option smartTriggers /--disable-smart-triggers bool :default true # Whether to use relevent triggers option relevantTriggers /--disable-relevant-triggers bool :default true prefer triggers that are more relevant based on SInE style analysis +option relationalTriggers --relational-triggers bool :default false + choose relational triggers such as x = f(y), x >= f(y) # Whether to consider terms in the bodies of quantifiers for matching option registerQuantBodyTerms --register-quant-body-terms bool :default false @@ -72,6 +80,8 @@ option cbqi --enable-cbqi/--disable-cbqi bool :default false turns on counterexample-based quantifier instantiation [off by default] /turns off counterexample-based quantifier instantiation +option recurseCbqi --cbqi-recurse bool :default false + turns on recursive counterexample-based quantifier instantiation option userPatternsQuant /--ignore-user-patterns bool :default true ignore user-provided patterns for quantifier instantiation @@ -88,6 +98,15 @@ option finiteModelFind --finite-model-find bool :default false option fmfModelBasedInst /--disable-fmf-mbqi bool :default true disable model-based quantifier instantiation for finite model finding +option fmfFullModelCheck --fmf-fmc bool :default false + enable full model check for finite model finding +option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true + disable simple models in full model check for finite model finding +option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true + disable covering simplification of fmc models +option fmfFmcInterval --fmf-fmc-interval bool :default false + construct interval models for fmc models + option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false only add one instantiation per quantifier per round for fmf option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false @@ -98,13 +117,17 @@ option fmfRelevantDomain --fmf-relevant-domain bool :default false use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) option fmfNewInstGen --fmf-new-inst-gen bool :default false use new inst gen technique for answering sat without exhaustive instantiation -option fmfInstGen /--disable-fmf-inst-gen bool :default true - disable Inst-Gen instantiation techniques for finite model finding +option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true + enable Inst-Gen instantiation techniques for finite model finding (default) +/disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques +option fmfBoundInt --fmf-bound-int bool :default false + finite model finding on bounded integer quantification + option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" policy for instantiating axioms diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 36db56d0d..59995a510 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -22,6 +22,102 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; + +bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) { + if ( n.getKind()==MULT ){ + if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){ + msum[n[1]] = n[0]; + return true; + } + }else{ + if( msum.find(n)==msum.end() ){ + msum[n] = Node::null(); + return true; + } + } + return false; +} + +bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) { + if ( n.getKind()==PLUS ){ + for( unsigned i=0; i<n.getNumChildren(); i++) { + if (!getMonomial( n[i], msum )){ + return false; + } + } + return true; + }else{ + return getMonomial( n, msum ); + } +} + +bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { + if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){ + if( getMonomialSum( lit[0], msum ) ){ + if( lit[1].isConst() ){ + if( !lit[1].getConst<Rational>().isZero() ){ + msum[Node::null()] = negate( lit[1] ); + } + return true; + } + } + } + return false; +} + +bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ) { + if( msum.find(v)!=msum.end() ){ + std::vector< Node > children; + Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst<Rational>(); + if ( r.sgn()!=0 ){ + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( it->first.isNull() || it->first!=v ){ + Node m; + if( !it->first.isNull() ){ + if ( !it->second.isNull() ){ + m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first ); + }else{ + m = it->first; + } + }else{ + m = it->second; + } + children.push_back(m); + } + } + veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : + (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); + if( !r.isNegativeOne() ){ + if( r.isOne() ){ + veq = negate(veq); + }else{ + //TODO + return false; + } + } + veq = Rewriter::rewrite( veq ); + veq = NodeManager::currentNM()->mkNode( k, r.sgn()==1 ? v : veq, r.sgn()==1 ? veq : v ); + return true; + } + return false; + }else{ + return false; + } +} + +Node QuantArith::negate( Node t ) { + Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); + tt = Rewriter::rewrite( tt ); + return tt; +} + +Node QuantArith::offset( Node t, int i ) { + Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t ); + tt = Rewriter::rewrite( tt ); + return tt; +} + + void QuantRelevance::registerQuantifier( Node f ){ //compute symbols in f std::vector< Node > syms; @@ -93,13 +189,13 @@ QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){ Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; if( it->first.getKind()==EQUAL ){ - if( it->first[0].hasAttribute(InstConstantAttribute()) ){ - if( !it->first[1].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(it->first[0]) ){ + if( !quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){ d_phase_reqs_equality_term[ it->first[0] ] = it->first[1]; d_phase_reqs_equality[ it->first[0] ] = it->second; Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; } - }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){ + }else if( quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){ d_phase_reqs_equality_term[ it->first[1] ] = it->first[0]; d_phase_reqs_equality[ it->first[1] ] = it->second; Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 6a5726cc7..86c7bc3a0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -28,6 +28,18 @@ namespace CVC4 { namespace theory { +class QuantArith +{ +public: + static bool getMonomial( Node n, std::map< Node, Node >& msum ); + static bool getMonomialSum( Node n, std::map< Node, Node >& msum ); + static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); + static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ); + static Node negate( Node t ); + static Node offset( Node t, int i ); +}; + + class QuantRelevance { private: diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 5bdce5fac..909c9c388 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -32,6 +32,10 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){ Trace("quant-attr") << "Set conjecture " << n << std::endl; ConjectureAttribute ca; n.setAttribute( ca, true ); + }else if( attr=="rr_priority" ){ + //Trace("quant-attr") << "Set rr priority " << n << std::endl; + //RrPriorityAttribute rra; + } }else{ for( size_t i=0; i<n.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 878d3ac50..1aebbfcc5 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -34,6 +34,10 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; struct ConjectureAttributeId {}; typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; +/** Attribute priority for rewrite rules */ +//struct RrPriorityAttributeId {}; +//typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute; + struct QuantifiersAttributes { /** set user attribute diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 5c71f6e6f..e27897a96 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -211,10 +211,6 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { if( in.hasAttribute(NestedQuantAttribute()) ){ setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) ); } - if( in.hasAttribute(InstConstantAttribute()) ){ - InstConstantAttribute ica; - ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) ); - } Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; Trace("quantifiers-rewrite") << " to " << std::endl; Trace("quantifiers-rewrite") << ret << std::endl; @@ -311,7 +307,7 @@ Node QuantifiersRewriter::computeSimpleIteLift( Node body ) { } Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ - Trace("var-elim-quant") << "Compute var elimination for " << body << std::endl; + Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; QuantPhaseReq qpr( body ); std::vector< Node > vars; std::vector< Node > subs; @@ -918,7 +914,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ - return !options::finiteModelFind(); + return options::simpleIteLiftQuant();//!options::finiteModelFind(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant() && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 2b011552c..b079ae75c 100644..100755 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -24,175 +24,159 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; +void RelevantDomain::RDomain::merge( RDomain * r ) { + Assert( !d_parent ); + Assert( !r->d_parent ); + d_parent = r; + for( unsigned i=0; i<d_terms.size(); i++ ){ + r->addTerm( d_terms[i] ); + } + d_terms.clear(); +} + +void RelevantDomain::RDomain::addTerm( Node t ) { + if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){ + d_terms.push_back( t ); + } +} + +RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() { + if( !d_parent ){ + return this; + }else{ + RDomain * p = d_parent->getParent(); + d_parent = p; + return p; + } +} + +void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) { + std::map< Node, Node > rterms; + for( unsigned i=0; i<d_terms.size(); i++ ){ + Node r = d_terms[i]; + if( !TermDb::hasInstConstAttr( d_terms[i] ) ){ + r = fm->getRepresentative( d_terms[i] ); + } + if( rterms.find( r )==rterms.end() ){ + rterms[r] = d_terms[i]; + } + } + d_terms.clear(); + for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){ + d_terms.push_back( it->second ); + } +} + + + RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){ } +RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) { + if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){ + d_rel_doms[n][i] = new RDomain; + d_rn_map[d_rel_doms[n][i]] = n; + d_ri_map[d_rel_doms[n][i]] = i; + } + return d_rel_doms[n][i]->getParent(); +} + void RelevantDomain::compute(){ - Trace("rel-dom") << "compute relevant domain" << std::endl; - d_quant_inst_domain.clear(); + for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){ + for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + it2->second->reset(); + } + } for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ Node f = d_model->getAssertedQuantifier( i ); - d_quant_inst_domain[f].resize( f[0].getNumChildren() ); + Node icf = d_qe->getTermDatabase()->getInstConstantBody( f ); + Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl; + computeRelevantDomain( icf, true, true ); } - Trace("rel-dom") << "account for ground terms" << std::endl; - //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment) - for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin(); - it != d_model->d_uf_model_tree.end(); ++it ){ + + Trace("rel-dom-debug") << "account for ground terms" << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = d_model->d_uf_terms.begin(); it != d_model->d_uf_terms.end(); ++it ){ Node op = it->first; - for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){ - Node n = d_model->d_uf_terms[op][i]; - //add arguments to domain - for( int j=0; j<(int)n.getNumChildren(); j++ ){ - if( d_model->d_rep_set.hasType( n[j].getType() ) ){ - Node ra = d_model->getRepresentative( n[j] ); - int raIndex = d_model->d_rep_set.getIndexFor( ra ); - if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground domain: rep set does not contain : " << ra << std::endl; - Assert( raIndex!=-1 ); - if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){ - d_active_domain[op][j].push_back( raIndex ); - } + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + //if it is a non-redundant term + if( !n.getAttribute(NoMatchAttribute()) ){ + for( unsigned j=0; j<n.getNumChildren(); j++ ){ + RDomain * rf = getRDomain( op, j ); + rf->addTerm( n[j] ); } } - //add to range - Node r = d_model->getRepresentative( n ); - int raIndex = d_model->d_rep_set.getIndexFor( r ); - if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground range: rep set does not contain : " << r << std::endl; - Assert( raIndex!=-1 ); - if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){ - d_active_range[op].push_back( raIndex ); - } } } - Trace("rel-dom") << "do quantifiers" << std::endl; - //find fixed point for relevant domain computation - bool success; - do{ - success = true; - for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ - Node f = d_model->getAssertedQuantifier( i ); - //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment) - if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getInstConstantBody( f ), Node::null(), -1, f ) ){ - success = false; - } - //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment) - RepDomain range; - if( extendFunctionDomains( d_qe->getTermDatabase()->getInstConstantBody( f ), range ) ){ - success = false; - } - } - }while( !success ); - Trace("rel-dom") << "done compute relevant domain" << std::endl; - /* - //debug printing - Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl; - if( useRelInstDomain ){ - Trace("rel-dom") << "Relevant domain : " << std::endl; - for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){ - Trace("rel-dom") << " " << i << " : "; - for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){ - Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " "; + //print debug + for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){ + Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl; + for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + Trace("rel-dom") << " " << it2->first << " : "; + RDomain * r = it2->second; + RDomain * rp = r->getParent(); + if( r==rp ){ + r->removeRedundantTerms( d_model ); + for( unsigned i=0; i<r->d_terms.size(); i++ ){ + Trace("rel-dom") << r->d_terms[i] << " "; + } + }else{ + Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) "; } Trace("rel-dom") << std::endl; } } - */ + } -bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){ - bool domainChanged = false; - if( n.getKind()==INST_CONSTANT ){ - bool domainSet = false; - int vi = n.getAttribute(InstVarNumAttribute()); - Assert( !parent.isNull() ); - if( parent.getKind()==APPLY_UF ){ - //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument - Node op = parent.getOperator(); - if( d_active_domain.find( op )!=d_active_domain.end() ){ - for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){ - int d = d_active_domain[op][arg][i]; - if( std::find( d_quant_inst_domain[f][vi].begin(), d_quant_inst_domain[f][vi].end(), d )== - d_quant_inst_domain[f][vi].end() ){ - d_quant_inst_domain[f][vi].push_back( d ); - domainChanged = true; - } - } - domainSet = true; - } - } - if( !domainSet ){ - //otherwise, we must consider the entire domain - TypeNode tn = n.getType(); - if( d_quant_inst_domain_complete[f].find( vi )==d_quant_inst_domain_complete[f].end() ){ - if( d_model->d_rep_set.hasType( tn ) ){ - //it is the complete domain - d_quant_inst_domain[f][vi].clear(); - for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){ - d_quant_inst_domain[f][vi].push_back( i ); - } - domainChanged = true; +void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { + + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( n.getKind()==APPLY_UF ){ + RDomain * rf = getRDomain( n.getOperator(), i ); + if( n[i].getKind()==INST_CONSTANT ){ + Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] ); + //merge the RDomains + unsigned id = n[i].getAttribute(InstVarNumAttribute()); + Trace("rel-dom-debug") << n[i] << " is variable # " << id << " for " << q; + Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl; + RDomain * rq = getRDomain( q, id ); + if( rf!=rq ){ + rq->merge( rf ); } - d_quant_inst_domain_complete[f][vi] = true; + }else{ + //term to add + rf->addTerm( n[i] ); } } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( computeRelevantInstantiationDomain( n[i], n, i, f ) ){ - domainChanged = true; - } + + //TODO + if( n[i].getKind()!=FORALL ){ + bool newHasPol = hasPol; + bool newPol = pol; + computeRelevantDomain( n[i], newHasPol, newPol ); } } - return domainChanged; } -bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ - if( n.getKind()==INST_CONSTANT ){ - Node f = n.getAttribute(InstConstantAttribute()); - int var = n.getAttribute(InstVarNumAttribute()); - range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() ); - return false; +Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) { + RDomain * rf = getRDomain( f, i ); + Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl; + if( !d_qe->getEqualityQuery()->getEngine()->hasTerm( r ) || rf->hasTerm( r ) ){ + return r; }else{ - Node op; - if( n.getKind()==APPLY_UF ){ - op = n.getOperator(); - } - bool domainChanged = false; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - RepDomain childRange; - if( extendFunctionDomains( n[i], childRange ) ){ - domainChanged = true; - } - if( n.getKind()==APPLY_UF ){ - if( d_active_domain.find( op )!=d_active_domain.end() ){ - for( int j=0; j<(int)childRange.size(); j++ ){ - int v = childRange[j]; - if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){ - d_active_domain[op][i].push_back( v ); - domainChanged = true; - } - } - }else{ - //do this? - } - } - } - //get the range - if( n.hasAttribute(InstConstantAttribute()) ){ - if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){ - range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() ); - }else{ - //infinite range? - } - }else{ - Node r = d_model->getRepresentative( n ); - int index = d_model->d_rep_set.getIndexFor( r ); - if( index==-1 ){ - //we consider all ground terms in bodies of quantifiers to be the first ground representative - range.push_back( 0 ); - }else{ - range.push_back( index ); + Node rr = d_model->getRepresentative( r ); + eq::EqClassIterator eqc( rr, d_qe->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + if( rf->hasTerm( en ) ){ + return en; } + ++eqc; } - return domainChanged; + //otherwise, may be equal to some non-ground term + + return r; } -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 6fc035e8a..c4345f828 100644..100755 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -26,25 +26,33 @@ namespace quantifiers { class RelevantDomain { private: + class RDomain + { + public: + RDomain() : d_parent( NULL ) {} + void reset() { d_parent = NULL; d_terms.clear(); } + RDomain * d_parent; + std::vector< Node > d_terms; + void merge( RDomain * r ); + void addTerm( Node t ); + RDomain * getParent(); + void removeRedundantTerms( FirstOrderModel * fm ); + bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } + }; + std::map< Node, std::map< int, RDomain * > > d_rel_doms; + std::map< RDomain *, Node > d_rn_map; + std::map< RDomain *, int > d_ri_map; + RDomain * getRDomain( Node n, int i ); QuantifiersEngine* d_qe; FirstOrderModel* d_model; - - //the domain of the arguments for each operator - std::map< Node, std::map< int, RepDomain > > d_active_domain; - //the range for each operator - std::map< Node, RepDomain > d_active_range; - //for computing relevant instantiation domain, return true if changed - bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ); - //for computing extended - bool extendFunctionDomains( Node n, RepDomain& range ); + void computeRelevantDomain( Node n, bool hasPol, bool pol ); public: RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ); virtual ~RelevantDomain(){} //compute the relevant domain void compute(); - //relevant instantiation domain for each quantifier - std::map< Node, std::vector< RepDomain > > d_quant_inst_domain; - std::map< Node, std::map< int, bool > > d_quant_inst_domain_complete; + + Node getRelevantTerm( Node f, int i, Node r ); };/* class RelevantDomain */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp new file mode 100755 index 000000000..107a99014 --- /dev/null +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -0,0 +1,184 @@ +/********************* */ +/*! \file bounded_integers.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Rewrite engine module + ** + ** This class manages rewrite rules for quantifiers + **/ + +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/inst_match_generator.h" +#include "theory/theory_engine.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +struct PrioritySort { + std::vector< double > d_priority; + bool operator() (int i,int j) { + return d_priority[i] < d_priority[j]; + } +}; + + +RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { + +} + +double RewriteEngine::getPriority( Node f ) { + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Node rrr = rr[2]; + Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl; + bool deterministic = rrr[1].getKind()!=OR; + if( rrr.getKind()==RR_REWRITE ){ + return deterministic ? 0.0 : 3.0; + }else if( rrr.getKind()==RR_DEDUCTION ){ + return deterministic ? 1.0 : 4.0; + }else if( rrr.getKind()==RR_REDUCTION ){ + return deterministic ? 2.0 : 5.0; + }else{ + return 6.0; + } +} + +void RewriteEngine::check( Theory::Effort e ) { + if( e==Theory::EFFORT_LAST_CALL ){ + if( !d_quantEngine->getModel()->isModelSet() ){ + d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true ); + } + if( d_true.isNull() ){ + d_true = NodeManager::currentNM()->mkConst( true ); + } + std::vector< Node > priority_order; + PrioritySort ps; + std::vector< int > indicies; + for( int i=0; i<(int)d_rr_quant.size(); i++ ){ + ps.d_priority.push_back( getPriority( d_rr_quant[i] ) ); + indicies.push_back( i ); + } + std::sort( indicies.begin(), indicies.end(), ps ); + for( unsigned i=0; i<indicies.size(); i++ ){ + priority_order.push_back( d_rr_quant[indicies[i]] ); + } + + //apply rewrite rules + int addedLemmas = 0; + //per priority level + int index = 0; + bool success = true; + while( success && index<(int)priority_order.size() ) { + addedLemmas += checkRewriteRule( priority_order[index] ); + index++; + if( index<(int)priority_order.size() ){ + success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] ); + } + } + + Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl; + if (addedLemmas==0) { + }else{ + //otherwise, the search will continue + d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); + } + } +} + +int RewriteEngine::checkRewriteRule( Node f ) { + Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl; + int addedLemmas = 0; + //reset triggers + Node rr = f.getAttribute(QRewriteRuleAttribute()); + if( d_rr_triggers.find(f)==d_rr_triggers.end() ){ + std::vector< inst::Trigger * > triggers; + if( f.getNumChildren()==3 ){ + for(unsigned i=0; i<f[2].getNumChildren(); i++ ){ + Node pat = f[2][i]; + std::vector< Node > nodes; + Trace("rewrite-engine-trigger") << "Trigger is : "; + for( int j=0; j<(int)pat.getNumChildren(); j++ ){ + Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f ); + nodes.push_back( p ); + Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " "; + } + Trace("rewrite-engine-trigger") << std::endl; + Assert( inst::Trigger::isUsableTrigger( nodes, f ) ); + inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false ); + tr->getGenerator()->setActiveAdd(false); + triggers.push_back( tr ); + } + } + d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() ); + } + for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){ + Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl; + d_rr_triggers[f][i]->resetInstantiationRound(); + d_rr_triggers[f][i]->reset( Node::null() ); + bool success; + do + { + InstMatch m; + success = d_rr_triggers[f][i]->getNextMatch( f, m ); + if( success ){ + //see if instantiation is true in the model + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Node rrg = rr[1]; + std::vector< Node > vars; + std::vector< Node > terms; + d_quantEngine->computeTermVector( f, m, vars, terms ); + Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl; + Node inst = d_rr_guard[f]; + inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl; + FirstOrderModel * fm = d_quantEngine->getModel(); + Node v = fm->getValue( inst ); + Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl; + if( v==d_true ){ + Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl; + if( d_quantEngine->addInstantiation( f, m ) ){ + addedLemmas++; + Trace("rewrite-engine-inst-debug") << "success" << std::endl; + //set the no-match attribute (the term is rewritten and can be ignored) + //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl; + //if( !m.d_matched.isNull() ){ + // NoMatchAttribute nma; + // m.d_matched.setAttribute(nma,true); + //} + }else{ + Trace("rewrite-engine-inst-debug") << "failure." << std::endl; + } + } + } + }while(success); + } + Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl; + return addedLemmas; +} + +void RewriteEngine::registerQuantifier( Node f ) { + if( f.hasAttribute(QRewriteRuleAttribute()) ){ + Trace("rewrite-engine") << "Register quantifier " << f << std::endl; + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Trace("rewrite-engine") << " rewrite rule is : " << rr << std::endl; + d_rr_quant.push_back( f ); + d_rr_guard[f] = rr[1]; + Trace("rewrite-engine") << " guard is : " << d_rr_guard[f] << std::endl; + } +} + +void RewriteEngine::assertNode( Node n ) { + +} + diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h new file mode 100755 index 000000000..2d9d751c2 --- /dev/null +++ b/src/theory/quantifiers/rewrite_engine.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \file bounded_integers.h +** \verbatim +** Original author: Andrew Reynolds +** This file is part of the CVC4 project. +** Copyright (c) 2009-2013 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief This class manages integer bounds for quantifiers +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__REWRITE_ENGINE_H +#define __CVC4__REWRITE_ENGINE_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/trigger.h" + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class RewriteEngine : public QuantifiersModule +{ + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + std::vector< Node > d_rr_quant; + std::map< Node, Node > d_rr_guard; + Node d_true; + /** explicitly provided patterns */ + std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; + double getPriority( Node f ); +private: + int checkRewriteRule( Node f ); +public: + RewriteEngine( context::Context* c, QuantifiersEngine* qe ); + + void check( Theory::Effort e ); + void registerQuantifier( Node f ); + void assertNode( Node n ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp new file mode 100755 index 000000000..507a50838 --- /dev/null +++ b/src/theory/quantifiers/symmetry_breaking.cpp @@ -0,0 +1,314 @@ +/********************* */ +/*! \file symmetry_breaking.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-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief symmetry breaking module + ** + **/ + +#include <vector> + +#include "theory/quantifiers/symmetry_breaking.h" +#include "theory/rewriter.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" +#include "util/sort_inference.h" +#include "theory/uf/theory_uf_strong_solver.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace std; + +namespace CVC4 { + + +SubsortSymmetryBreaker::SubsortSymmetryBreaker(QuantifiersEngine* qe, context::Context* c) : +d_qe(qe), d_conflict(c,false) { + d_true = NodeManager::currentNM()->mkConst( true ); +} + +eq::EqualityEngine * SubsortSymmetryBreaker::getEqualityEngine() { + return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine(); +} + +bool SubsortSymmetryBreaker::areEqual( Node n1, Node n2 ) { + return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 ); +} + +bool SubsortSymmetryBreaker::areDisequal( Node n1, Node n2 ) { + return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false ); +} + + +Node SubsortSymmetryBreaker::getRepresentative( Node n ) { + return getEqualityEngine()->getRepresentative( n ); +} + +uf::StrongSolverTheoryUF * SubsortSymmetryBreaker::getStrongSolver() { + return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getStrongSolver(); +} + +SubsortSymmetryBreaker::TypeInfo::TypeInfo( context::Context * c ) : +d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false) { +} + +SubsortSymmetryBreaker::SubSortInfo::SubSortInfo( context::Context * c ) : +d_dom_constants( c ), d_first_active( c, 0 ){ + d_dc_nodes = 0; +} + +unsigned SubsortSymmetryBreaker::SubSortInfo::getNumDomainConstants() { + if( d_nodes.empty() ){ + return 0; + }else{ + return 1 + d_dom_constants.size(); + } +} + +Node SubsortSymmetryBreaker::SubSortInfo::getDomainConstant( int i ) { + if( i==0 ){ + return d_nodes[0]; + }else{ + Assert( i<=(int)d_dom_constants.size() ); + return d_dom_constants[i-1]; + } +} + +Node SubsortSymmetryBreaker::SubSortInfo::getFirstActive(eq::EqualityEngine * ee) { + if( d_first_active.get()<(int)d_nodes.size() ){ + Node fa = d_nodes[d_first_active.get()]; + return ee->hasTerm( fa ) ? fa : Node::null(); + }else{ + return Node::null(); + } +} + +SubsortSymmetryBreaker::TypeInfo * SubsortSymmetryBreaker::getTypeInfo( TypeNode tn ) { + if( d_t_info.find( tn )==d_t_info.end() ){ + d_t_info[tn] = new TypeInfo( d_qe->getSatContext() ); + } + return d_t_info[tn]; +} + +SubsortSymmetryBreaker::SubSortInfo * SubsortSymmetryBreaker::getSubSortInfo( TypeNode tn, int sid ) { + if( d_type_info.find( sid )==d_type_info.end() ){ + d_type_info[sid] = new SubSortInfo( d_qe->getSatContext() ); + d_sub_sorts[tn].push_back( sid ); + d_sid_to_type[sid] = tn; + } + return d_type_info[sid]; +} + +void SubsortSymmetryBreaker::newEqClass( Node n ) { + Trace("sym-break-temp") << "New eq class " << n << std::endl; + if( !d_conflict ){ + TypeNode tn = n.getType(); + SortInference * si = d_qe->getTheoryEngine()->getSortInference(); + if( si->isWellSorted( n ) ){ + int sid = si->getSortId( n ); + Trace("sym-break-debug") << "SSB: New eq class " << n << " : " << n.getType() << " : " << sid << std::endl; + SubSortInfo * ti = getSubSortInfo( tn, sid ); + if( std::find( ti->d_nodes.begin(), ti->d_nodes.end(), n )==ti->d_nodes.end() ){ + if( ti->d_nodes.empty() ){ + //for first subsort, we add unit equality + if( d_sub_sorts[tn][0]!=sid ){ + Trace("sym-break-temp") << "Do sym break unit with " << d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() << std::endl; + //add unit symmetry breaking lemma + Node eq = n.eqNode( d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() ); + eq = Rewriter::rewrite( eq ); + d_unit_lemmas.push_back( eq ); + Trace("sym-break-lemma") << "*** SymBreak : Unit lemma (" << sid << "==" << d_sub_sorts[tn][0] << ") : " << eq << std::endl; + d_pending_lemmas.push_back( eq ); + } + Trace("sym-break-dc") << "* Set first domain constant : " << n << " for " << tn << " : " << sid << std::endl; + ti->d_dc_nodes++; + } + ti->d_node_to_id[n] = ti->d_nodes.size(); + ti->d_nodes.push_back( n ); + } + TypeInfo * tti = getTypeInfo( tn ); + if( !tti->d_has_dom_const_sort.get() ){ + tti->d_has_dom_const_sort.set( true ); + tti->d_max_dom_const_sort.set( sid ); + } + } + } + Trace("sym-break-temp") << "Done new eq class" << std::endl; +} + + + +void SubsortSymmetryBreaker::merge( Node a, Node b ) { + if( Trace.isOn("sym-break-debug") ){ + SortInference * si = d_qe->getTheoryEngine()->getSortInference(); + int as = si->getSortId( a ); + int bs = si->getSortId( b ); + Trace("sym-break-debug") << "SSB: New merge " << a.getType() << " :: " << a << " : " << as; + Trace("sym-break-debug") << " == " << b << " : " << bs << std::endl; + } +} + +void SubsortSymmetryBreaker::assertDisequal( Node a, Node b ) { + if( Trace.isOn("sym-break-debug") ){ + SortInference * si = d_qe->getTheoryEngine()->getSortInference(); + int as = si->getSortId( a ); + int bs = si->getSortId( b ); + Trace("sym-break-debug") << "SSB: New assert disequal " << a.getType() << " :: " << a << " : " << as; + Trace("sym-break-debug") << " != " << b << " : " << bs << std::endl; + } +} + +void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_card ){ + SubSortInfo * ti = getSubSortInfo( tn, sid ); + if( (int)ti->getNumDomainConstants()<curr_card ){ + //static int checkCount = 0; + //checkCount++; + //if( checkCount%1000==0 ){ + // std::cout << "Check count = " << checkCount << std::endl; + //} + + Trace("sym-break-dc-debug") << "Check for domain constants " << tn << " : " << sid << ", curr_card = " << curr_card << ", "; + Trace("sym-break-dc-debug") << "#domain constants = " << ti->getNumDomainConstants() << std::endl; + Node fa = ti->getFirstActive(getEqualityEngine()); + bool invalid = true; + while( invalid && !fa.isNull() && (int)ti->getNumDomainConstants()<curr_card ){ + invalid = false; + unsigned deq = 0; + for( unsigned i=0; i<ti->getNumDomainConstants(); i++ ){ + Node dc = ti->getDomainConstant( i ); + if( areEqual( fa, dc ) ){ + invalid = true; + break; + }else if( areDisequal( fa, dc ) ){ + deq++; + } + } + if( deq==ti->getNumDomainConstants() ){ + Trace("sym-break-dc") << "* Can infer domain constant #" << ti->getNumDomainConstants()+1; + Trace("sym-break-dc") << " : " << fa << " for " << tn << " : " << sid << std::endl; + //add to domain constants + ti->d_dom_constants.push_back( fa ); + if( ti->d_node_to_id[fa]>ti->d_dc_nodes ){ + Trace("sym-break-dc-debug") << "Swap nodes... " << ti->d_dc_nodes << " " << ti->d_node_to_id[fa] << " " << ti->d_nodes.size() << std::endl; + //swap + Node on = ti->d_nodes[ti->d_dc_nodes]; + int id = ti->d_node_to_id[fa]; + + ti->d_nodes[ti->d_dc_nodes] = fa; + ti->d_nodes[id] = on; + ti->d_node_to_id[fa] = ti->d_dc_nodes; + ti->d_node_to_id[on] = id; + } + ti->d_dc_nodes++; + Trace("sym-break-dc-debug") << "Get max type info..." << std::endl; + TypeInfo * tti = getTypeInfo( tn ); + Assert( tti->d_has_dom_const_sort.get() ); + int msid = tti->d_max_dom_const_sort.get(); + SubSortInfo * max_ti = getSubSortInfo( d_sid_to_type[msid], msid ); + Trace("sym-break-dc-debug") << "Swap nodes..." << std::endl; + //now, check if we can apply symmetry breaking to another sort + if( ti->getNumDomainConstants()>max_ti->getNumDomainConstants() ){ + Trace("sym-break-dc") << "Max domain constant subsort for " << tn << " becomes " << sid << std::endl; + tti->d_max_dom_const_sort.set( sid ); + }else if( ti!=max_ti ){ + //construct symmetry breaking lemma + //current domain constant must be disequal from all current ones + Trace("sym-break-dc") << "Get domain constant " << ti->getNumDomainConstants()-1; + Trace("sym-break-dc") << " from max_ti, " << max_ti->getNumDomainConstants() << std::endl; + //apply a symmetry breaking lemma + Node m = max_ti->getDomainConstant(ti->getNumDomainConstants()-1); + //if fa and m are disequal from all previous domain constants in the other sort + std::vector< Node > cc; + for( unsigned r=0; r<2; r++ ){ + Node n = ((r==0)==(msid>sid)) ? fa : m; + Node on = ((r==0)==(msid>sid)) ? m : fa; + SubSortInfo * t = ((r==0)==(msid>sid)) ? max_ti : ti; + for( unsigned i=0; i<t->d_node_to_id[on]; i++ ){ + cc.push_back( n.eqNode( t->d_nodes[i] ) ); + } + } + //then, we can assume fa = m + cc.push_back( fa.eqNode( m ) ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, cc ); + lem = Rewriter::rewrite( lem ); + if( std::find( d_lemmas.begin(), d_lemmas.end(), lem )==d_lemmas.end() ){ + d_lemmas.push_back( lem ); + Trace("sym-break-lemma") << "*** Symmetry break lemma for " << tn << " (" << sid << "==" << tti->d_max_dom_const_sort.get() << ") : "; + Trace("sym-break-lemma") << lem << std::endl; + d_pending_lemmas.push_back( lem ); + } + } + invalid = true; + } + if( invalid ){ + ti->d_first_active.set( ti->d_first_active + 1 ); + fa = ti->getFirstActive(getEqualityEngine()); + } + } + } +} + +void SubsortSymmetryBreaker::printDebugSubSortInfo( const char * c, TypeNode tn, int sid ) { + Trace(c) << "SubSortInfo( " << tn << ", " << sid << " ) = " << std::endl; + Trace(c) << " Domain constants : "; + SubSortInfo * ti = getSubSortInfo( tn, sid ); + for( NodeList::const_iterator it = ti->d_dom_constants.begin(); it != ti->d_dom_constants.end(); ++it ){ + Node dc = *it; + Trace(c) << dc << " "; + } + Trace(c) << std::endl; + Trace(c) << " First active node : " << ti->getFirstActive(getEqualityEngine()) << std::endl; +} + +bool SubsortSymmetryBreaker::check( Theory::Effort level ) { + + Trace("sym-break-debug") << "SymBreak : check " << level << std::endl; + /* + while( d_fact_index.get()<d_fact_list.size() ){ + Node f = d_fact_list[d_fact_index.get()]; + d_fact_index.set( d_fact_index.get() + 1 ); + if( f.getKind()==EQUAL ){ + merge( f[0], f[1] ); + }else if( f.getKind()==NOT && f[0].getKind()==EQUAL ){ + assertDisequal( f[0][0], f[0][1] ); + }else{ + newEqClass( f ); + } + } + */ + Trace("sym-break-debug") << "SymBreak : update first actives" << std::endl; + for( std::map< TypeNode, std::vector< int > >::iterator it = d_sub_sorts.begin(); it != d_sub_sorts.end(); ++it ){ + int card = getStrongSolver()->getCardinality( it->first ); + for( unsigned i=0; i<it->second.size(); i++ ){ + //check if the first active is disequal from all domain constants + processFirstActive( it->first, it->second[i], card ); + } + } + + + Trace("sym-break-debug") << "SymBreak : finished check, now flush lemmas... (#lemmas = " << d_pending_lemmas.size() << ")" << std::endl; + //flush pending lemmas + if( !d_pending_lemmas.empty() ){ + for( unsigned i=0; i<d_pending_lemmas.size(); i++ ){ + getStrongSolver()->getOutputChannel().lemma( d_pending_lemmas[i] ); + ++( getStrongSolver()->d_statistics.d_sym_break_lemmas ); + } + d_pending_lemmas.clear(); + return true; + }else{ + return false; + } +} + + + +} + diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h new file mode 100755 index 000000000..05461d378 --- /dev/null +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -0,0 +1,118 @@ +/********************* */ +/*! \file symmetry_breaking.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-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process step for first-order reasoning + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANT_SYMMETRY_BREAKING_H +#define __CVC4__QUANT_SYMMETRY_BREAKING_H + +#include "theory/theory.h" + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" + +#include "util/sort_inference.h" +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.h" + +namespace CVC4 { +namespace theory { + +namespace uf { + class StrongSolverTheoryUF; +} + +class SubsortSymmetryBreaker { + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + //typedef context::CDChunkList<int> IntList; + typedef context::CDList<Node> NodeList; + typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; +private: + /** quantifiers engine */ + QuantifiersEngine* d_qe; + eq::EqualityEngine * getEqualityEngine(); + bool areDisequal( Node n1, Node n2 ); + bool areEqual( Node n1, Node n2 ); + Node getRepresentative( Node n ); + uf::StrongSolverTheoryUF * getStrongSolver(); + std::vector< Node > d_unit_lemmas; + Node d_true; + context::CDO< bool > d_conflict; +public: + SubsortSymmetryBreaker( QuantifiersEngine* qe, context::Context* c ); + ~SubsortSymmetryBreaker(){} + +private: + class TypeInfo { + public: + TypeInfo( context::Context* c ); + context::CDO< int > d_max_dom_const_sort; + context::CDO< bool > d_has_dom_const_sort; + }; + class SubSortInfo { + public: + SubSortInfo( context::Context* c ); + //list of all nodes from this (sub)type + std::vector< Node > d_nodes; + //the current domain constants for this (sub)type + NodeList d_dom_constants; + //# nodes in d_nodes that have been domain constants, size of this distinct # of domain constants seen + unsigned d_dc_nodes; + //the node we are currently watching to become a domain constant + context::CDO< int > d_first_active; + //node to id + std::map< Node, unsigned > d_node_to_id; + Node getBaseConstant() { return d_nodes.empty() ? Node::null() : d_nodes[0]; } + bool hasDomainConstant( Node n ); + unsigned getNumDomainConstants(); + Node getDomainConstant( int i ); + Node getFirstActive(eq::EqualityEngine * ee); + }; + std::map< TypeNode, std::vector< int > > d_sub_sorts; + std::map< int, TypeNode > d_sid_to_type; + std::map< TypeNode, TypeInfo * > d_t_info; + std::map< int, SubSortInfo * > d_type_info; + + TypeInfo * getTypeInfo( TypeNode tn ); + SubSortInfo * getSubSortInfo( TypeNode tn, int sid ); + + void processFirstActive( TypeNode tn, int sid, int curr_card ); +private: + //void printDebugNodeInfo( const char * c, Node n ); + void printDebugSubSortInfo( const char * c, TypeNode tn, int sid ); + /** fact list */ + std::vector< Node > d_pending_lemmas; + std::vector< Node > d_lemmas; +public: + /** new node */ + void newEqClass( Node n ); + /** merge */ + void merge( Node a, Node b ); + /** assert disequal */ + void assertDisequal( Node a, Node b ); + /** check */ + bool check( Theory::Effort level ); +}; + +} +} + +#endif diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3153a3c64..e18a4e0dc 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -74,7 +74,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ //if this is an atomic trigger, consider adding it //Call the children? if( inst::Trigger::isAtomicTrigger( n ) ){ - if( !n.hasAttribute(InstConstantAttribute()) ){ + if( !TermDb::hasInstConstAttr(n) ){ Trace("term-db") << "register term in db " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; Node op = n.getOperator(); @@ -117,7 +117,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } } }else{ - if( options::efficientEMatching() && !n.hasAttribute(InstConstantAttribute())){ + if( options::efficientEMatching() && !TermDb::hasInstConstAttr(n)){ //Efficient e-matching must be notified //The term in triggers are not important here Debug("term-db") << "New in this branch term " << n << std::endl; @@ -167,7 +167,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ while( !eqc.isFinished() ){ Node en = (*eqc); computeModelBasisArgAttribute( en ); - if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ + if( en.getKind()==APPLY_UF && !TermDb::hasInstConstAttr(en) ){ if( !en.getAttribute(NoMatchAttribute()) ){ Node op = en.getOperator(); if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ @@ -194,14 +194,20 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){ Node mbt; - if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){ - std::stringstream ss; - ss << Expr::setlanguage(options::outputLanguage()); - ss << "e_" << tn; - mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" ); - Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl; + if( tn.isInteger() || tn.isReal() ){ + mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + }else if( !tn.isSort() ){ + mbt = tn.mkGroundTerm(); }else{ - mbt = d_type_map[ tn ][ 0 ]; + if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){ + std::stringstream ss; + ss << Expr::setlanguage(options::outputLanguage()); + ss << "e_" << tn; + mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" ); + Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl; + }else{ + mbt = d_type_map[ tn ][ 0 ]; + } } ModelBasisAttribute mba; mbt.setAttribute(mba,true); @@ -254,8 +260,7 @@ void TermDb::computeModelBasisArgAttribute( Node n ){ //determine if it has model basis attribute for( int j=0; j<(int)n.getNumChildren(); j++ ){ if( n[j].getAttribute(ModelBasisAttribute()) ){ - val = 1; - break; + val++; } } ModelBasisArgAttribute mbaa; @@ -276,33 +281,75 @@ void TermDb::makeInstantiationConstantsFor( Node f ){ //set the var number attribute InstVarNumAttribute ivna; ic.setAttribute(ivna,i); + InstConstantAttribute ica; + ic.setAttribute(ica,f); + //also set the no-match attribute + NoMatchAttribute nma; + ic.setAttribute(nma,true); } } } -void TermDb::setInstantiationConstantAttr( Node n, Node f ){ - if( !n.hasAttribute(InstConstantAttribute()) ){ - bool setAttr = false; - if( n.getKind()==INST_CONSTANT ){ - setAttr = true; - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - setInstantiationConstantAttr( n[i], f ); - if( n[i].hasAttribute(InstConstantAttribute()) ){ - setAttr = true; - } + +Node TermDb::getInstConstAttr( Node n ) { + if (!n.hasAttribute(InstConstantAttribute()) ){ + Node f; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + f = getInstConstAttr(n[i]); + if( !f.isNull() ){ + break; } } - if( setAttr ){ - InstConstantAttribute ica; - n.setAttribute(ica,f); + InstConstantAttribute ica; + n.setAttribute(ica,f); + if( !f.isNull() ){ //also set the no-match attribute NoMatchAttribute nma; n.setAttribute(nma,true); } } + return n.getAttribute(InstConstantAttribute()); +} + +bool TermDb::hasInstConstAttr( Node n ) { + return !getInstConstAttr(n).isNull(); +} + +bool TermDb::hasBoundVarAttr( Node n ) { + if( !n.getAttribute(HasBoundVarComputedAttribute()) ){ + bool hasBv = false; + if( n.getKind()==BOUND_VARIABLE ){ + hasBv = true; + }else{ + for (unsigned i=0; i<n.getNumChildren(); i++) { + if( hasBoundVarAttr(n[i]) ){ + hasBv = true; + break; + } + } + } + HasBoundVarAttribute hbva; + n.setAttribute(hbva, hasBv); + HasBoundVarComputedAttribute hbvca; + n.setAttribute(hbvca, true); + Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttribute()) << std::endl; + } + return n.getAttribute(HasBoundVarAttribute()); +} + +void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) { + if (n.getKind()==BOUND_VARIABLE ){ + if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){ + bvs.push_back( n ); + } + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++) { + getBoundVars(n[i], bvs); + } + } } + /** get the i^th instantiation constant of f */ Node TermDb::getInstantiationConstant( Node f, int i ) const { std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); @@ -348,7 +395,6 @@ Node TermDb::getCounterexampleLiteral( Node f ){ //otherwise, ensure literal Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() ); d_ce_lit[ f ] = ceLit; - setInstantiationConstantAttr( ceLit, f ); } return d_ce_lit[ f ]; } @@ -362,7 +408,6 @@ Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & var Node n2 = n.substitute( vars.begin(), vars.end(), inst_constants.begin(), inst_constants.end() ); - setInstantiationConstantAttr( n2, f ); return n2; } @@ -390,16 +435,19 @@ Node TermDb::getSkolemizedBody( Node f ){ Node TermDb::getFreeVariableForInstConstant( Node n ){ TypeNode tn = n.getType(); if( d_free_vars.find( tn )==d_free_vars.end() ){ - //if integer or real, make zero - if( tn.isInteger() || tn.isReal() ){ - Rational z(0); - d_free_vars[tn] = NodeManager::currentNM()->mkConst( z ); - }else{ - if( d_type_map[ tn ].empty() ){ - d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar_$$", tn, "is a free variable created by termdb" ); - Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl; + for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){ + if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){ + d_free_vars[tn] = d_type_map[ tn ][ i ]; + } + } + if( d_free_vars.find( tn )==d_free_vars.end() ){ + //if integer or real, make zero + if( tn.isInteger() || tn.isReal() ){ + Rational z(0); + d_free_vars[tn] = NodeManager::currentNM()->mkConst( z ); }else{ - d_free_vars[tn] = d_type_map[ tn ][ 0 ]; + d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar_$$", tn, "is a free variable created by termdb" ); + Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl; } } } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 231d0ee9e..1688479f3 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -59,6 +59,19 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; struct ModelBasisArgAttributeId {}; typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute; +struct HasBoundVarAttributeId {}; +typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute; +struct HasBoundVarComputedAttributeId {}; +typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute; + +//for rewrite rules +struct QRewriteRuleAttributeId {}; +typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute; + +//for bounded integers +struct BoundIntLitAttributeId {}; +typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute; + class QuantifiersEngine; @@ -83,10 +96,15 @@ public: };/* class TermArgTrie */ +namespace fmcheck { + class FullModelChecker; +} + class TermDb { friend class ::CVC4::theory::QuantifiersEngine; friend class ::CVC4::theory::inst::Trigger; friend class ::CVC4::theory::rrinst::Trigger; + friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -181,9 +199,15 @@ public: Node convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars, const std::vector<Node> & nvars); - /** set instantiation constant attr */ - void setInstantiationConstantAttr( Node n, Node f ); + static Node getInstConstAttr( Node n ); + static bool hasInstConstAttr( Node n ); +//for bound variables +public: + //does n have bound variables? + static bool hasBoundVarAttr( Node n ); + //get bound variables in n + static void getBoundVars( Node n, std::vector< Node >& bvs); //for skolem private: /** map from universal quantifiers to the list of skolem constants */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 9843cd09e..066282c2c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -65,7 +65,7 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { void TheoryQuantifiers::preRegisterTerm(TNode n) { Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; - if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){ + if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){ getQuantifiersEngine()->registerQuantifier( n ); } } @@ -149,7 +149,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){ void TheoryQuantifiers::assertUniversal( Node n ){ Assert( n.getKind()==FORALL ); - if( !n.hasAttribute(InstConstantAttribute()) ){ + if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ getQuantifiersEngine()->registerQuantifier( n ); getQuantifiersEngine()->assertNode( n ); } @@ -157,13 +157,13 @@ void TheoryQuantifiers::assertUniversal( Node n ){ void TheoryQuantifiers::assertExistential( Node n ){ Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !n[0].hasAttribute(InstConstantAttribute()) ){ + if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){ if( d_skolemized.find( n )==d_skolemized.end() ){ Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] ); NodeBuilder<> nb(kind::OR); nb << n[0] << body.notNode(); Node lem = nb; - Debug("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl; + Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl; d_out->lemma( lem ); d_skolemized[n] = true; } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index cab94fb5c..39063942d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -28,8 +28,6 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; -//#define NESTED_PATTERN_SELECTION - /** trigger class constructor */ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : d_quantEngine( qe ), d_f( f ){ @@ -46,7 +44,7 @@ d_quantEngine( qe ), d_f( f ){ d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes[0], qe ); - d_mg->setActiveAdd(); + d_mg->setActiveAdd(true); } }else{ d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); @@ -55,7 +53,7 @@ d_quantEngine( qe ), d_f( f ){ } }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); - d_mg->setActiveAdd(); + d_mg->setActiveAdd(true); } if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ @@ -75,6 +73,7 @@ d_quantEngine( qe ), d_f( f ){ qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() ); } } + Trace("trigger-debug") << "Finished making trigger." << std::endl; } void Trigger::resetInstantiationRound(){ @@ -126,7 +125,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& qe->getTermDatabase()->computeVarContains( temp[i] ); for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; - if( v.getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(v)==f ){ if( vars.find( v )==vars.end() ){ varCount++; vars[ v ] = true; @@ -146,6 +145,12 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } if( varCount<f[0].getNumChildren() ){ + Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl; + for( unsigned i=0; i<nodes.size(); i++) { + Trace("trigger-debug") << nodes[i] << " "; + } + Trace("trigger-debug") << std::endl; + //do not generate multi-trigger if it does not contain all variables return NULL; }else{ @@ -225,7 +230,7 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ } bool Trigger::isUsable( Node n, Node f ){ - if( n.getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(n)==f ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ if( !isUsable( n[i], f ) ){ @@ -249,11 +254,71 @@ bool Trigger::isUsable( Node n, Node f ){ } } +bool nodeContainsVar( Node n, Node v ){ + if( n==v) { + return true; + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++) { + if( nodeContainsVar(n[i], v) ){ + return true; + } + } + return false; + } +} + +Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { + if( options::relationalTriggers() ){ + if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ + Node rtr; + for( unsigned i=0; i<2; i++) { + unsigned j = (i==0) ? 1 : 0; + if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) { + rtr = n; + break; + } + } + if( n[0].getType().isInteger() ){ + //try to rearrange? + std::map< Node, Node > m; + if (QuantArith::getMonomialSumLit(n, m) ){ + for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){ + if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){ + Node veq; + if( QuantArith::isolate( it->first, m, veq, n.getKind() ) ){ + int vti = veq[0]==it->first ? 1 : 0; + if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){ + rtr = veq; + } + } + } + } + } + } + if( !rtr.isNull() ){ + Trace("relational-trigger") << "Relational trigger : " << std::endl; + Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl; + Trace("relational-trigger") << " in quantifier " << f << std::endl; + if( hasPol ){ + Trace("relational-trigger") << " polarity : " << pol << std::endl; + } + Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr; + return rtr2; + } + } + } + bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); + Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; + if( usable ){ + return n; + }else{ + return Node::null(); + } +} + bool Trigger::isUsableTrigger( Node n, Node f ){ - //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF; - bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); - Trace("usable") << n << " usable : " << usable << std::endl; - return usable; + Node nu = getIsUsableTrigger(n,f); + return !nu.isNull(); } bool Trigger::isAtomicTrigger( Node n ){ @@ -263,7 +328,7 @@ bool Trigger::isAtomicTrigger( Node n ){ bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){ + if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){ return false; } } @@ -274,55 +339,51 @@ bool Trigger::isSimpleTrigger( Node n ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ +bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; + bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol; + bool newPol = n.getKind()==NOT ? !pol : pol; if( tstrt==TS_MIN_TRIGGER ){ if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ); - return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ); -#else return false; -#endif }else{ bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; + bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ retVal = true; } } if( retVal ){ return true; - }else if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; - return true; }else{ - return false; + Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + if( !nu.isNull() ){ + patMap[ nu ] = true; + return true; + }else{ + return false; + } } } }else{ bool retVal = false; - if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; + Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + if( !nu.isNull() ){ + patMap[ nu ] = true; if( tstrt==TS_MAX_TRIGGER ){ return true; }else{ retVal = true; } } - if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){ - // retVal = true; - //} - if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){ - retVal = true; - } -#endif - }else{ + if( n.getKind()!=FORALL ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; + bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ retVal = true; } } @@ -367,7 +428,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } } - collectPatTerms2( qe, f, n, patMap, tstrt ); + collectPatTerms2( qe, f, n, patMap, tstrt, true, true ); for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ if( it->second ){ patTerms.push_back( it->first ); @@ -380,9 +441,9 @@ bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeff Assert( coeffs.empty() ); NodeBuilder<> t(kind::PLUS); for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){ if( n[i].getKind()==INST_CONSTANT ){ - if( n[i].getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){ coeffs[ n[i] ] = Node::null(); }else{ coeffs.clear(); @@ -405,13 +466,13 @@ bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeff } return true; }else if( n.getKind()==MULT ){ - if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){ - if( !n[1].hasAttribute(InstConstantAttribute()) ){ + if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){ + if( !quantifiers::TermDb::hasInstConstAttr(n[1]) ){ coeffs[ n[0] ] = n[1]; return true; } - }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){ - if( !n[0].hasAttribute(InstConstantAttribute()) ){ + }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){ + if( !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ coeffs[ n[1] ] = n[0]; return true; } diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index ca9124751..28fb2acda 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -92,8 +92,9 @@ public: private: /** is subterm of trigger usable */ static bool isUsable( Node n, Node f ); + static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ); + static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ); public: //different strategies for choosing trigger terms enum { |