-/********************* */\r
-/*! \file bounded_integers.cpp\r
- ** \verbatim\r
- ** Original author: Andrew Reynolds\r
- ** This file is part of the CVC4 project.\r
- ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
- ** See the file COPYING in the top-level source directory for licensing\r
- ** information.\endverbatim\r
- **\r
- ** \brief Bounded integers module\r
- **\r
- ** This class manages integer bounds for quantifiers\r
- **/\r
-\r
-#include "theory/quantifiers/bounded_integers.h"\r
-#include "theory/quantifiers/quant_util.h"\r
-#include "theory/quantifiers/first_order_model.h"\r
-#include "theory/quantifiers/model_engine.h"\r
-\r
-using namespace CVC4;\r
-using namespace std;\r
-using namespace CVC4::theory;\r
-using namespace CVC4::theory::quantifiers;\r
-using namespace CVC4::kind;\r
-\r
-void BoundedIntegers::RangeModel::initialize() {\r
- //add initial split lemma\r
- Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) );\r
- ltr = Rewriter::rewrite( ltr );\r
- Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr << std::endl;\r
- d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );\r
- Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;\r
- d_range_literal[-1] = ltr_lit;\r
- d_lit_to_range[ltr_lit] = -1;\r
- d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;\r
- //register with bounded integers\r
- Trace("bound-int-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;\r
- d_bi->addLiteralFromRange(ltr_lit, d_range);\r
-}\r
-\r
-void BoundedIntegers::RangeModel::assertNode(Node n) {\r
- bool pol = n.getKind()!=NOT;\r
- Node nlit = n.getKind()==NOT ? n[0] : n;\r
- if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){\r
- Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";\r
- Trace("bound-int-assert") << ", found literal " << nlit;\r
- Trace("bound-int-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;\r
- d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]);\r
- if( pol!=d_lit_to_pol[nlit] ){\r
- //check if we need a new split?\r
- if( !d_has_range ){\r
- bool needsRange = true;\r
- for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){\r
- if( d_range_assertions.find( it->first )==d_range_assertions.end() ){\r
- needsRange = false;\r
- break;\r
- }\r
- }\r
- if( needsRange ){\r
- allocateRange();\r
- }\r
- }\r
- }else{\r
- if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){\r
- Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;\r
- d_curr_range = d_lit_to_range[nlit];\r
- }\r
- //set the range\r
- d_has_range = true;\r
- }\r
- }else{\r
- Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl;\r
- exit(0);\r
- }\r
-}\r
-\r
-void BoundedIntegers::RangeModel::allocateRange() {\r
- d_curr_max++;\r
- int newBound = d_curr_max;\r
- Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;\r
- //TODO: newBound should be chosen in a smarter way\r
- Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );\r
- ltr = Rewriter::rewrite( ltr );\r
- Trace("bound-int-lemma") << " *** bound int: split on " << ltr << std::endl;\r
- d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );\r
- Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;\r
- d_range_literal[newBound] = ltr_lit;\r
- d_lit_to_range[ltr_lit] = newBound;\r
- d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;\r
- //register with bounded integers\r
- d_bi->addLiteralFromRange(ltr_lit, d_range);\r
-}\r
-\r
-Node BoundedIntegers::RangeModel::getNextDecisionRequest() {\r
- //request the current cardinality as a decision literal, if not already asserted\r
- for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){\r
- int i = it->second;\r
- if( !d_has_range || i<d_curr_range ){\r
- Node rn = it->first;\r
- Assert( !rn.isNull() );\r
- if( d_range_assertions.find( rn )==d_range_assertions.end() ){\r
- if (!d_lit_to_pol[it->first]) {\r
- rn = rn.negate();\r
- }\r
- Trace("bound-int-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;\r
- return rn;\r
- }\r
- }\r
- }\r
- return Node::null();\r
-}\r
-\r
-\r
-BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :\r
-QuantifiersModule(qe), d_assertions(c){\r
-\r
-}\r
-\r
-bool BoundedIntegers::isBound( Node f, Node v ) {\r
- return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();\r
-}\r
-\r
-bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {\r
- if( b.getKind()==BOUND_VARIABLE ){\r
- if( !isBound( f, b ) ){\r
- return true;\r
- }\r
- }else{\r
- for( unsigned i=0; i<b.getNumChildren(); i++ ){\r
- if( hasNonBoundVar( f, b[i] ) ){\r
- return true;\r
- }\r
- }\r
- }\r
- return false;\r
-}\r
-\r
-void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,\r
- std::map< int, std::map< Node, Node > >& bound_lit_map,\r
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map ) {\r
- if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){\r
- std::map< Node, Node > msum;\r
- if (QuantArith::getMonomialSumLit( lit, msum )){\r
- Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;\r
- for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
- Trace("bound-int-debug") << " ";\r
- if( !it->second.isNull() ){\r
- Trace("bound-int-debug") << it->second;\r
- if( !it->first.isNull() ){\r
- Trace("bound-int-debug") << " * ";\r
- }\r
- }\r
- if( !it->first.isNull() ){\r
- Trace("bound-int-debug") << it->first;\r
- }\r
- Trace("bound-int-debug") << std::endl;\r
- }\r
- Trace("bound-int-debug") << std::endl;\r
- for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
- if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){\r
- Node veq;\r
- if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){\r
- Node n1 = veq[0];\r
- Node n2 = veq[1];\r
- if(pol){\r
- //flip\r
- n1 = veq[1];\r
- n2 = veq[0];\r
- if( n1.getKind()==BOUND_VARIABLE ){\r
- n2 = QuantArith::offset( n2, 1 );\r
- }else{\r
- n1 = QuantArith::offset( n1, -1 );\r
- }\r
- veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );\r
- }\r
- Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;\r
- Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;\r
- if( !isBound( f, bv ) ){\r
- if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {\r
- Trace("bound-int-debug") << "The bound is relevant." << std::endl;\r
- int loru = n1.getKind()==BOUND_VARIABLE ? 0 : 1;\r
- d_bounds[loru][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);\r
- bound_lit_map[loru][bv] = lit;\r
- bound_lit_pol_map[loru][bv] = pol;\r
- }\r
- }\r
- }\r
- }\r
- }\r
- }\r
- }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {\r
- Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;\r
- exit(0);\r
- }\r
-}\r
-\r
-void BoundedIntegers::process( Node f, Node n, bool pol,\r
- std::map< int, std::map< Node, Node > >& bound_lit_map,\r
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){\r
- if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){\r
- for( unsigned i=0; i<n.getNumChildren(); i++) {\r
- bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol;\r
- process( f, n[i], newPol, bound_lit_map, bound_lit_pol_map );\r
- }\r
- }else if( n.getKind()==NOT ){\r
- process( f, n[0], !pol, bound_lit_map, bound_lit_pol_map );\r
- }else {\r
- processLiteral( f, n, pol, bound_lit_map, bound_lit_pol_map );\r
- }\r
-}\r
-\r
-void BoundedIntegers::check( Theory::Effort e ) {\r
-\r
-}\r
-\r
-\r
-void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {\r
- d_lit_to_ranges[lit].push_back(r);\r
- //check if it is already asserted?\r
- if(d_assertions.find(lit)!=d_assertions.end()){\r
- d_rms[r]->assertNode( d_assertions[lit] ? lit : lit.negate() );\r
- }\r
-}\r
-\r
-void BoundedIntegers::registerQuantifier( Node f ) {\r
- Trace("bound-int") << "Register quantifier " << f << std::endl;\r
- bool hasIntType = false;\r
- int finiteTypes = 0;\r
- std::map< Node, int > numMap;\r
- for( unsigned i=0; i<f[0].getNumChildren(); i++) {\r
- numMap[f[0][i]] = i;\r
- if( f[0][i].getType().isInteger() ){\r
- hasIntType = true;\r
- }\r
- else if( f[0][i].getType().isSort() ){\r
- finiteTypes++;\r
- }\r
- }\r
- if( hasIntType ){\r
- bool success;\r
- do{\r
- std::map< int, std::map< Node, Node > > bound_lit_map;\r
- std::map< int, std::map< Node, bool > > bound_lit_pol_map;\r
- success = false;\r
- process( f, f[1], true, bound_lit_map, bound_lit_pol_map );\r
- for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){\r
- Node v = it->first;\r
- if( !isBound(f,v) ){\r
- if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){\r
- d_set[f].push_back(v);\r
- d_set_nums[f].push_back(numMap[v]);\r
- success = true;\r
- //set Attributes on literals\r
- for( unsigned b=0; b<2; b++ ){\r
- Assert( bound_lit_map[b].find( v )!=bound_lit_map[b].end() );\r
- Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() );\r
- BoundIntLitAttribute bila;\r
- bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 );\r
- }\r
- Trace("bound-int") << "Variable " << v << " is bound because of literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;\r
- }\r
- }\r
- }\r
- }while( success );\r
- Trace("bound-int") << "Bounds are : " << std::endl;\r
- for( unsigned i=0; i<d_set[f].size(); i++) {\r
- Node v = d_set[f][i];\r
- Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );\r
- d_range[f][v] = Rewriter::rewrite( r );\r
- Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;\r
- }\r
- if( d_set[f].size()==(f[0].getNumChildren()-finiteTypes) ){\r
- d_bound_quants.push_back( f );\r
- for( unsigned i=0; i<d_set[f].size(); i++) {\r
- Node v = d_set[f][i];\r
- Node r = d_range[f][v];\r
- if( quantifiers::TermDb::hasBoundVarAttr(r) ){\r
- //introduce a new bound\r
- Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );\r
- d_nground_range[f][v] = d_range[f][v];\r
- d_range[f][v] = new_range;\r
- r = new_range;\r
- }\r
- if( r.getKind()!=CONST_RATIONAL ){\r
- if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){\r
- Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl;\r
- d_ranges.push_back( r );\r
- d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );\r
- d_rms[r]->initialize();\r
- }\r
- }\r
- }\r
- }\r
- }\r
-}\r
-\r
-void BoundedIntegers::assertNode( Node n ) {\r
- Trace("bound-int-assert") << "Assert " << n << std::endl;\r
- Node nlit = n.getKind()==NOT ? n[0] : n;\r
- if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){\r
- Trace("bound-int-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl;\r
- for( unsigned i=0; i<d_lit_to_ranges[nlit].size(); i++) {\r
- Node r = d_lit_to_ranges[nlit][i];\r
- Trace("bound-int-assert") << " ...this is a bounding literal for " << r << std::endl;\r
- d_rms[r]->assertNode( n );\r
- }\r
- }\r
- d_assertions[nlit] = n.getKind()!=NOT;\r
-}\r
-\r
-Node BoundedIntegers::getNextDecisionRequest() {\r
- Trace("bound-int-dec") << "bi: Get next decision request?" << std::endl;\r
- for( unsigned i=0; i<d_ranges.size(); i++) {\r
- Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();\r
- if (!d.isNull()) {\r
- return d;\r
- }\r
- }\r
- return Node::null();\r
-}\r
-\r
-void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {\r
- l = d_bounds[0][f][v];\r
- u = d_bounds[1][f][v];\r
- if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){\r
- //must create substitution\r
- std::vector< Node > vars;\r
- std::vector< Node > subs;\r
- Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;\r
- for( unsigned i=0; i<d_set[f].size(); i++) {\r
- if( d_set[f][i]!=v ){\r
- Trace("bound-int-rsi") << "Look up the value for " << d_set[f][i] << " " << rsi->d_var_order[d_set_nums[f][i]] << std::endl;\r
- Trace("bound-int-rsi") << "term : " << rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]) << std::endl;\r
- vars.push_back(d_set[f][i]);\r
- subs.push_back(rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]));\r
- }else{\r
- break;\r
- }\r
- }\r
- Trace("bound-int-rsi") << "Do substitution..." << std::endl;\r
- //check if it has been instantiated\r
- if (!vars.empty() && !d_bnd_it[f][v].hasInstantiated(subs)){\r
- //must add the lemma\r
- Node nn = d_nground_range[f][v];\r
- nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
- Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] );\r
- Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;\r
- d_quantEngine->getOutputChannel().lemma(lem);\r
- l = Node::null();\r
- u = Node::null();\r
- return;\r
- }else{\r
- u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
- l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
- }\r
- }\r
- Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;\r
- l = d_quantEngine->getModel()->getCurrentModelValue( l );\r
- u = d_quantEngine->getModel()->getCurrentModelValue( u );\r
- Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;\r
- return;\r
-}\r
-\r
-bool BoundedIntegers::isGroundRange(Node f, Node v) {\r
- return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v));\r
-}
\ No newline at end of file
+/********************* */
+/*! \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();
+ }
+ }
+ }
+ }
+ }
+}
+
+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::getBoundValues( 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() );
+ }
+ }
+ 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));
+}
-\r
-/********************* */\r
-/*! \file full_model_check.cpp\r
- ** \verbatim\r
- ** Original author: Andrew Reynolds\r
- ** This file is part of the CVC4 project.\r
- ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
- ** See the file COPYING in the top-level source directory for licensing\r
- ** information.\endverbatim\r
- **\r
- ** \brief Implementation of full model check class\r
- **/\r
-\r
-#include "theory/quantifiers/full_model_check.h"\r
-#include "theory/quantifiers/first_order_model.h"\r
-#include "theory/quantifiers/options.h"\r
-\r
-using namespace std;\r
-using namespace CVC4;\r
-using namespace CVC4::kind;\r
-using namespace CVC4::context;\r
-using namespace CVC4::theory;\r
-using namespace CVC4::theory::quantifiers;\r
-using namespace CVC4::theory::inst;\r
-using namespace CVC4::theory::quantifiers::fmcheck;\r
-\r
-struct ModelBasisArgSort\r
-{\r
- std::vector< Node > d_terms;\r
- bool operator() (int i,int j) {\r
- return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <\r
- d_terms[j].getAttribute(ModelBasisArgAttribute()) );\r
- }\r
-};\r
-\r
-\r
-struct ConstRationalSort\r
-{\r
- std::vector< Node > d_terms;\r
- bool operator() (int i, int j) {\r
- return (d_terms[i].getConst<Rational>() < d_terms[j].getConst<Rational>() );\r
- }\r
-};\r
-\r
-\r
-bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {\r
- if (index==(int)c.getNumChildren()) {\r
- return d_data!=-1;\r
- }else{\r
- TypeNode tn = c[index].getType();\r
- Node st = m->getStar(tn);\r
- if(d_child.find(st)!=d_child.end()) {\r
- if( d_child[st].hasGeneralization(m, c, index+1) ){\r
- return true;\r
- }\r
- }\r
- if( c[index]!=st && d_child.find( c[index] )!=d_child.end() ){\r
- if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){\r
- return true;\r
- }\r
- }\r
- if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){\r
- //for star: check if all children are defined and have generalizations\r
- if( options::fmfFmcCoverSimplify() && c[index]==st ){\r
- //check if all children exist and are complete\r
- int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);\r
- if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){\r
- bool complete = true;\r
- for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
- if( !m->isStar(it->first) ){\r
- if( !it->second.hasGeneralization(m, c, index+1) ){\r
- complete = false;\r
- break;\r
- }\r
- }\r
- }\r
- if( complete ){\r
- return true;\r
- }\r
- }\r
- }\r
- }\r
-\r
- return false;\r
- }\r
-}\r
-\r
-int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {\r
- Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl;\r
- if (index==(int)inst.size()) {\r
- return d_data;\r
- }else{\r
- int minIndex = -1;\r
- if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){\r
- for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
- if( !m->isInterval( it->first ) ){\r
- std::cout << "Not an interval during getGenIndex " << it->first << std::endl;\r
- exit( 11 );\r
- }\r
- //check if it is in the range\r
- if( m->isInRange(inst[index], it->first ) ){\r
- int gindex = it->second.getGeneralizationIndex(m, inst, index+1);\r
- if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){\r
- minIndex = gindex;\r
- }\r
- }\r
- }\r
- }else{\r
- Node st = m->getStar(inst[index].getType());\r
- if(d_child.find(st)!=d_child.end()) {\r
- minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);\r
- }\r
- Node cc = inst[index];\r
- if( cc!=st && d_child.find( cc )!=d_child.end() ){\r
- int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);\r
- if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){\r
- minIndex = gindex;\r
- }\r
- }\r
- }\r
- return minIndex;\r
- }\r
-}\r
-\r
-void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) {\r
- if (index==(int)c.getNumChildren()) {\r
- if(d_data==-1) {\r
- d_data = data;\r
- }\r
- }\r
- else {\r
- d_child[ c[index] ].addEntry(m,c,v,data,index+1);\r
- if( d_complete==0 ){\r
- d_complete = -1;\r
- }\r
- }\r
-}\r
-\r
-void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {\r
- if (index==(int)c.getNumChildren()) {\r
- if( d_data!=-1) {\r
- if( is_gen ){\r
- gen.push_back(d_data);\r
- }\r
- compat.push_back(d_data);\r
- }\r
- }else{\r
- if (m->isStar(c[index])) {\r
- for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
- it->second.getEntries(m, c, compat, gen, index+1, is_gen );\r
- }\r
- }else{\r
- Node st = m->getStar(c[index].getType());\r
- if(d_child.find(st)!=d_child.end()) {\r
- d_child[st].getEntries(m, c, compat, gen, index+1, false);\r
- }\r
- if( d_child.find( c[index] )!=d_child.end() ){\r
- d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen);\r
- }\r
- }\r
-\r
- }\r
-}\r
-\r
-void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) {\r
- if (index==(int)c.getNumChildren()) {\r
- if( d_data!=-1 ){\r
- indices.push_back( d_data );\r
- }\r
- }else{\r
- for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
- it->second.collectIndices(c, index+1, indices );\r
- }\r
- }\r
-}\r
-\r
-bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) {\r
- if( d_complete==-1 ){\r
- d_complete = 1;\r
- if (index<(int)c.getNumChildren()) {\r
- Node st = m->getStar(c[index].getType());\r
- if(d_child.find(st)!=d_child.end()) {\r
- if (!d_child[st].isComplete(m, c, index+1)) {\r
- d_complete = 0;\r
- }\r
- }else{\r
- d_complete = 0;\r
- }\r
- }\r
- }\r
- return d_complete==1;\r
-}\r
-\r
-bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {\r
- if (d_et.hasGeneralization(m, c)) {\r
- Trace("fmc-debug") << "Already has generalization, skip." << std::endl;\r
- return false;\r
- }\r
- int newIndex = (int)d_cond.size();\r
- if (!d_has_simplified) {\r
- std::vector<int> compat;\r
- std::vector<int> gen;\r
- d_et.getEntries(m, c, compat, gen);\r
- for( unsigned i=0; i<compat.size(); i++) {\r
- if( d_status[compat[i]]==status_unk ){\r
- if( d_value[compat[i]]!=v ){\r
- d_status[compat[i]] = status_non_redundant;\r
- }\r
- }\r
- }\r
- for( unsigned i=0; i<gen.size(); i++) {\r
- if( d_status[gen[i]]==status_unk ){\r
- if( d_value[gen[i]]==v ){\r
- d_status[gen[i]] = status_redundant;\r
- }\r
- }\r
- }\r
- d_status.push_back( status_unk );\r
- }\r
- d_et.addEntry(m, c, v, newIndex);\r
- d_cond.push_back(c);\r
- d_value.push_back(v);\r
- return true;\r
-}\r
-\r
-Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {\r
- int gindex = d_et.getGeneralizationIndex(m, inst);\r
- if (gindex!=-1) {\r
- return d_value[gindex];\r
- }else{\r
- Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl;\r
- return Node::null();\r
- }\r
-}\r
-\r
-int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) {\r
- return d_et.getGeneralizationIndex(m, inst);\r
-}\r
-\r
-void Def::basic_simplify( FirstOrderModelFmc * m ) {\r
- d_has_simplified = true;\r
- std::vector< Node > cond;\r
- cond.insert( cond.end(), d_cond.begin(), d_cond.end() );\r
- d_cond.clear();\r
- std::vector< Node > value;\r
- value.insert( value.end(), d_value.begin(), d_value.end() );\r
- d_value.clear();\r
- d_et.reset();\r
- for (unsigned i=0; i<d_status.size(); i++) {\r
- if( d_status[i]!=status_redundant ){\r
- addEntry(m, cond[i], value[i]);\r
- }\r
- }\r
- d_status.clear();\r
-}\r
-\r
-void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {\r
- basic_simplify( m );\r
-\r
- //check if the last entry is not all star, if so, we can make the last entry all stars\r
- if( !d_cond.empty() ){\r
- bool last_all_stars = true;\r
- Node cc = d_cond[d_cond.size()-1];\r
- for( unsigned i=0; i<cc.getNumChildren(); i++ ){\r
- if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){\r
- last_all_stars = false;\r
- break;\r
- }\r
- }\r
- if( !last_all_stars ){\r
- Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl;\r
- Trace("fmc-cover-simplify") << "Before: " << std::endl;\r
- debugPrint("fmc-cover-simplify",Node::null(), mc);\r
- Trace("fmc-cover-simplify") << std::endl;\r
- std::vector< Node > cond;\r
- cond.insert( cond.end(), d_cond.begin(), d_cond.end() );\r
- d_cond.clear();\r
- std::vector< Node > value;\r
- value.insert( value.end(), d_value.begin(), d_value.end() );\r
- d_value.clear();\r
- d_et.reset();\r
- d_has_simplified = false;\r
- //change the last to all star\r
- std::vector< Node > nc;\r
- nc.push_back( cc.getOperator() );\r
- for( unsigned j=0; j< cc.getNumChildren(); j++){\r
- nc.push_back(m->getStarElement(cc[j].getType()));\r
- }\r
- cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );\r
- //re-add the entries\r
- for (unsigned i=0; i<cond.size(); i++) {\r
- addEntry(m, cond[i], value[i]);\r
- }\r
- Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;\r
- basic_simplify( m );\r
- Trace("fmc-cover-simplify") << "After: " << std::endl;\r
- debugPrint("fmc-cover-simplify",Node::null(), mc);\r
- Trace("fmc-cover-simplify") << std::endl;\r
- }\r
- }\r
-}\r
-\r
-void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {\r
- if (!op.isNull()) {\r
- Trace(tr) << "Model for " << op << " : " << std::endl;\r
- }\r
- for( unsigned i=0; i<d_cond.size(); i++) {\r
- //print the condition\r
- if (!op.isNull()) {\r
- Trace(tr) << op;\r
- }\r
- m->debugPrintCond(tr, d_cond[i], true);\r
- Trace(tr) << " -> ";\r
- m->debugPrint(tr, d_value[i]);\r
- Trace(tr) << std::endl;\r
- }\r
-}\r
-\r
-\r
-FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :\r
-QModelBuilder( c, qe ){\r
- d_true = NodeManager::currentNM()->mkConst(true);\r
- d_false = NodeManager::currentNM()->mkConst(false);\r
-}\r
-\r
-bool FullModelChecker::optBuildAtFullModel() {\r
- //need to build after full model has taken effect if we are constructing interval models\r
- // this is because we need to have a constant in all integer equivalence classes\r
- return options::fmfFmcInterval();\r
-}\r
-\r
-void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){\r
- FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();\r
- if( fullModel==optBuildAtFullModel() ){\r
- Trace("fmc") << "---Full Model Check reset() " << std::endl;\r
- fm->initialize( d_considerAxioms );\r
- d_quant_models.clear();\r
- d_rep_ids.clear();\r
- d_star_insts.clear();\r
- //process representatives\r
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();\r
- it != fm->d_rep_set.d_type_reps.end(); ++it ){\r
- if( it->first.isSort() ){\r
- Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;\r
- Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);\r
- Node rmbt = fm->getUsedRepresentative( mbt);\r
- int mbt_index = -1;\r
- Trace("fmc") << " Model basis term : " << mbt << std::endl;\r
- for( size_t a=0; a<it->second.size(); a++ ){\r
- Node r = fm->getUsedRepresentative( it->second[a] );\r
- std::vector< Node > eqc;\r
- ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );\r
- Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);\r
- Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";\r
- //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";\r
- Trace("fmc-model-debug") << " {";\r
- //find best selection for representative\r
- for( size_t i=0; i<eqc.size(); i++ ){\r
- Trace("fmc-model-debug") << eqc[i] << ", ";\r
- }\r
- Trace("fmc-model-debug") << "}" << std::endl;\r
-\r
- //if this is the model basis eqc, replace with actual model basis term\r
- if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {\r
- fm->d_model_basis_rep[it->first] = r;\r
- r = mbt;\r
- mbt_index = a;\r
- }\r
- d_rep_ids[it->first][r] = (int)a;\r
- }\r
- Trace("fmc-model-debug") << std::endl;\r
-\r
- if (mbt_index==-1) {\r
- std::cout << " WARNING: model basis term is not a representative!" << std::endl;\r
- exit(0);\r
- }else{\r
- Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;\r
- }\r
- }\r
- }\r
- //also process non-rep set sorts\r
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
- Node op = it->first;\r
- TypeNode tno = op.getType();\r
- for( unsigned i=0; i<tno.getNumChildren(); i++) {\r
- initializeType( fm, tno[i] );\r
- }\r
- }\r
- //now, make models\r
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
- Node op = it->first;\r
- //reset the model\r
- fm->d_models[op]->reset();\r
-\r
- Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;\r
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
- Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]);\r
- Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;\r
- }\r
- Trace("fmc-model-debug") << std::endl;\r
-\r
-\r
- std::vector< Node > add_conds;\r
- std::vector< Node > add_values;\r
- bool needsDefault = true;\r
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
- Node n = fm->d_uf_terms[op][i];\r
- if( !n.getAttribute(NoMatchAttribute()) ){\r
- add_conds.push_back( n );\r
- add_values.push_back( n );\r
- }\r
- }\r
- //possibly get default\r
- if( needsDefault ){\r
- Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
- //add default value if necessary\r
- if( fm->hasTerm( nmb ) ){\r
- Trace("fmc-model-debug") << "Add default " << nmb << std::endl;\r
- add_conds.push_back( nmb );\r
- add_values.push_back( nmb );\r
- }else{\r
- Node vmb = getSomeDomainElement(fm, nmb.getType());\r
- Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";\r
- Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;\r
- add_conds.push_back( nmb );\r
- add_values.push_back( vmb );\r
- }\r
- }\r
-\r
- std::vector< Node > conds;\r
- std::vector< Node > values;\r
- std::vector< Node > entry_conds;\r
- //get the entries for the mdoel\r
- for( size_t i=0; i<add_conds.size(); i++ ){\r
- Node c = add_conds[i];\r
- Node v = add_values[i];\r
- std::vector< Node > children;\r
- std::vector< Node > entry_children;\r
- children.push_back(op);\r
- entry_children.push_back(op);\r
- bool hasNonStar = false;\r
- for( unsigned i=0; i<c.getNumChildren(); i++) {\r
- Node ri = fm->getUsedRepresentative( c[i]);\r
- if( !ri.getType().isSort() && !ri.isConst() ){\r
- Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;\r
- }\r
- children.push_back(ri);\r
- if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){\r
- if (fm->isModelBasisTerm(ri) ) {\r
- ri = fm->getStar( ri.getType() );\r
- }else{\r
- hasNonStar = true;\r
- }\r
- }\r
- entry_children.push_back(ri);\r
- }\r
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
- Node nv = fm->getUsedRepresentative( v );\r
- if( !nv.getType().isSort() && !nv.isConst() ){\r
- Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;\r
- }\r
- Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );\r
- if( std::find(conds.begin(), conds.end(), n )==conds.end() ){\r
- Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
- conds.push_back(n);\r
- values.push_back(nv);\r
- entry_conds.push_back(en);\r
- }\r
- else {\r
- Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
- }\r
- }\r
-\r
-\r
- //sort based on # default arguments\r
- std::vector< int > indices;\r
- ModelBasisArgSort mbas;\r
- for (int i=0; i<(int)conds.size(); i++) {\r
- d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );\r
- mbas.d_terms.push_back(conds[i]);\r
- indices.push_back(i);\r
- }\r
- std::sort( indices.begin(), indices.end(), mbas );\r
-\r
- for (int i=0; i<(int)indices.size(); i++) {\r
- fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);\r
- }\r
-\r
-\r
- if( options::fmfFmcInterval() ){\r
- Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;\r
- fm->d_models[op]->debugPrint("fmc-interval-model", op, this);\r
- Trace("fmc-interval-model") << std::endl;\r
- std::vector< int > indices;\r
- for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){\r
- indices.push_back( i );\r
- }\r
- std::map< int, std::map< int, Node > > changed_vals;\r
- makeIntervalModel( fm, op, indices, 0, changed_vals );\r
-\r
- std::vector< Node > conds;\r
- std::vector< Node > values;\r
- for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){\r
- if( changed_vals.find(i)==changed_vals.end() ){\r
- conds.push_back( fm->d_models[op]->d_cond[i] );\r
- }else{\r
- std::vector< Node > children;\r
- children.push_back( op );\r
- for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){\r
- if( changed_vals[i].find(j)==changed_vals[i].end() ){\r
- children.push_back( fm->d_models[op]->d_cond[i][j] );\r
- }else{\r
- children.push_back( changed_vals[i][j] );\r
- }\r
- }\r
- Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
- conds.push_back( nc );\r
- Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";\r
- debugPrintCond("fmc-interval-model", nc, true );\r
- Trace("fmc-interval-model") << std::endl;\r
- }\r
- values.push_back( fm->d_models[op]->d_value[i] );\r
- }\r
- fm->d_models[op]->reset();\r
- for( unsigned i=0; i<conds.size(); i++ ){\r
- fm->d_models[op]->addEntry(fm, conds[i], values[i] );\r
- }\r
- }\r
-\r
- Trace("fmc-model-simplify") << "Before simplification : " << std::endl;\r
- fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);\r
- Trace("fmc-model-simplify") << std::endl;\r
-\r
- Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;\r
- fm->d_models[op]->simplify( this, fm );\r
-\r
- fm->d_models[op]->debugPrint("fmc-model", op, this);\r
- Trace("fmc-model") << std::endl;\r
- }\r
- }\r
- if( fullModel ){\r
- //make function values\r
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){\r
- m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );\r
- }\r
- TheoryEngineModelBuilder::processBuildModel( m, fullModel );\r
- //mark that the model has been set\r
- fm->markModelSet();\r
- //debug the model\r
- debugModel( fm );\r
- }\r
-}\r
-\r
-void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){\r
- if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){\r
- Trace("fmc") << "Initialize type " << tn << std::endl;\r
- Node mbn;\r
- if (!fm->d_rep_set.hasType(tn)) {\r
- mbn = fm->getSomeDomainElement(tn);\r
- }else{\r
- mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
- }\r
- Node mbnr = fm->getUsedRepresentative( mbn );\r
- fm->d_model_basis_rep[tn] = mbnr;\r
- Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;\r
- }\r
-}\r
-\r
-void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {\r
- Trace(tr) << "(";\r
- for( unsigned j=0; j<n.getNumChildren(); j++) {\r
- if( j>0 ) Trace(tr) << ", ";\r
- debugPrint(tr, n[j], dispStar);\r
- }\r
- Trace(tr) << ")";\r
-}\r
-\r
-void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {\r
- FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();\r
- if( n.isNull() ){\r
- Trace(tr) << "null";\r
- }\r
- else if(fm->isStar(n) && dispStar) {\r
- Trace(tr) << "*";\r
- }\r
- else if(fm->isInterval(n)) {\r
- debugPrint(tr, n[0], dispStar );\r
- Trace(tr) << "...";\r
- debugPrint(tr, n[1], dispStar );\r
- }else{\r
- TypeNode tn = n.getType();\r
- if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
- if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {\r
- Trace(tr) << d_rep_ids[tn][n];\r
- }else{\r
- Trace(tr) << n;\r
- }\r
- }else{\r
- Trace(tr) << n;\r
- }\r
- }\r
-}\r
-\r
-\r
-bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {\r
- Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;\r
- if( optUseModel() ){\r
- FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();\r
- if (effort==0) {\r
- //register the quantifier\r
- if (d_quant_cond.find(f)==d_quant_cond.end()) {\r
- std::vector< TypeNode > types;\r
- for(unsigned i=0; i<f[0].getNumChildren(); i++){\r
- types.push_back(f[0][i].getType());\r
- d_quant_var_id[f][f[0][i]] = i;\r
- }\r
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );\r
- Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );\r
- d_quant_cond[f] = op;\r
- }\r
- //make sure all types are set\r
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){\r
- initializeType( fmfmc, f[0][i].getType() );\r
- }\r
-\r
- //model check the quantifier\r
- doCheck(fmfmc, f, d_quant_models[f], f[1]);\r
- Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;\r
- d_quant_models[f].debugPrint("fmc", Node::null(), this);\r
- Trace("fmc") << std::endl;\r
-\r
- //consider all entries going to non-true\r
- for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {\r
- if( d_quant_models[f].d_value[i]!=d_true) {\r
- Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;\r
- bool hasStar = false;\r
- std::vector< Node > inst;\r
- for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {\r
- if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {\r
- hasStar = true;\r
- inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));\r
- }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){\r
- hasStar = true;\r
- //if interval, find a sample point\r
- if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){\r
- if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){\r
- inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType()));\r
- }else{\r
- Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],\r
- NodeManager::currentNM()->mkConst( Rational(1) ) );\r
- nn = Rewriter::rewrite( nn );\r
- inst.push_back( nn );\r
- }\r
- }else{\r
- inst.push_back(d_quant_models[f].d_cond[i][j][0]);\r
- }\r
- }else{\r
- inst.push_back(d_quant_models[f].d_cond[i][j]);\r
- }\r
- }\r
- bool addInst = true;\r
- if( hasStar ){\r
- //try obvious (specified by inst)\r
- Node ev = d_quant_models[f].evaluate(fmfmc, inst);\r
- if (ev==d_true) {\r
- addInst = false;\r
- }\r
- }else{\r
- //for debugging\r
- if (Trace.isOn("fmc-test-inst")) {\r
- Node ev = d_quant_models[f].evaluate(fmfmc, inst);\r
- if( ev==d_true ){\r
- std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;\r
- exit(0);\r
- }else{\r
- Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;\r
- }\r
- }\r
- }\r
- if( addInst ){\r
- InstMatch m;\r
- for( unsigned j=0; j<inst.size(); j++) {\r
- m.set( d_qe, f, j, inst[j] );\r
- }\r
- d_triedLemmas++;\r
- if( d_qe->addInstantiation( f, m ) ){\r
- d_addedLemmas++;\r
- }else{\r
- //this can happen if evaluation is unknown\r
- //might try it next effort level\r
- d_star_insts[f].push_back(i);\r
- }\r
- }else{\r
- //might try it next effort level\r
- d_star_insts[f].push_back(i);\r
- }\r
- }\r
- }\r
- }else{\r
- if (!d_star_insts[f].empty()) {\r
- Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;\r
- Trace("fmc-exh") << "Definition was : " << std::endl;\r
- d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);\r
- Trace("fmc-exh") << std::endl;\r
- Def temp;\r
- //simplify the exceptions?\r
- for( int i=(d_star_insts[f].size()-1); i>=0; i--) {\r
- //get witness for d_star_insts[f][i]\r
- int j = d_star_insts[f][i];\r
- if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
- if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){\r
- //something went wrong, resort to exhaustive instantiation\r
- return false;\r
- }\r
- }\r
- }\r
- }\r
- }\r
- return true;\r
- }else{\r
- return false;\r
- }\r
-}\r
-\r
-bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {\r
- RepSetIterator riter( d_qe, &(fm->d_rep_set) );\r
- Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";\r
- debugPrintCond("fmc-exh", c, true);\r
- Trace("fmc-exh")<< std::endl;\r
- Trace("fmc-exh-debug") << "Set interval domains..." << std::endl;\r
- //set the bounds on the iterator based on intervals\r
- for( unsigned i=0; i<c.getNumChildren(); i++ ){\r
- if( c[i].getType().isInteger() ){\r
- if( fm->isInterval(c[i]) ){\r
- for( unsigned b=0; b<2; b++ ){\r
- if( !fm->isStar(c[i][b]) ){\r
- riter.d_bounds[b][i] = c[i][b];\r
- }\r
- }\r
- }else if( !fm->isStar(c[i]) ){\r
- riter.d_bounds[0][i] = c[i];\r
- riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );\r
- }\r
- }\r
- }\r
- Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;\r
- //initialize\r
- if( riter.setQuantifier( f ) ){\r
- Trace("fmc-exh-debug") << "Set element domains..." << std::endl;\r
- //set the domains based on the entry\r
- for (unsigned i=0; i<c.getNumChildren(); i++) {\r
- if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {\r
- TypeNode tn = c[i].getType();\r
- if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
- if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){\r
- //add the full range\r
- }else{\r
- if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {\r
- riter.d_domain[i].clear();\r
- riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);\r
- }else{\r
- return false;\r
- }\r
- }\r
- }else{\r
- return false;\r
- }\r
- }\r
- }\r
- int addedLemmas = 0;\r
- //now do full iteration\r
- while( !riter.isFinished() ){\r
- d_triedLemmas++;\r
- Trace("fmc-exh-debug") << "Inst : ";\r
- std::vector< Node > inst;\r
- for( int i=0; i<riter.getNumTerms(); i++ ){\r
- //m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );\r
- Node r = fm->getUsedRepresentative( riter.getTerm( i ) );\r
- debugPrint("fmc-exh-debug", r);\r
- Trace("fmc-exh-debug") << " ";\r
- inst.push_back(r);\r
- }\r
- int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);\r
- Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();\r
- Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];\r
- if (ev!=d_true) {\r
- InstMatch m;\r
- for( int i=0; i<riter.getNumTerms(); i++ ){\r
- m.set( d_qe, f, i, riter.getTerm( i ) );\r
- }\r
- Trace("fmc-exh-debug") << ", add!";\r
- //add as instantiation\r
- if( d_qe->addInstantiation( f, m ) ){\r
- Trace("fmc-exh-debug") << " ...success.";\r
- addedLemmas++;\r
- }\r
- }else{\r
- Trace("fmc-exh-debug") << ", already true";\r
- }\r
- Trace("fmc-exh-debug") << std::endl;\r
- int index = riter.increment();\r
- Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;\r
- if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {\r
- Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;\r
- riter.increment2( index-1 );\r
- }\r
- }\r
- d_addedLemmas += addedLemmas;\r
- return true;\r
- }else{\r
- return false;\r
- }\r
-}\r
-\r
-void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {\r
- Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;\r
- //first check if it is a bounding literal\r
- if( n.hasAttribute(BoundIntLitAttribute()) ){\r
- Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;\r
- d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );\r
- }else if( n.getKind() == kind::BOUND_VARIABLE ){\r
- Trace("fmc-debug") << "Add default entry..." << std::endl;\r
- d.addEntry(fm, mkCondDefault(fm, f), n);\r
- }\r
- else if( n.getKind() == kind::NOT ){\r
- //just do directly\r
- doCheck( fm, f, d, n[0] );\r
- doNegate( d );\r
- }\r
- else if( n.getKind() == kind::FORALL ){\r
- d.addEntry(fm, mkCondDefault(fm, f), Node::null());\r
- }\r
- else if( n.getType().isArray() ){\r
- //make the definition\r
- Node r = fm->getRepresentative(n);\r
- Trace("fmc-debug") << "Representative for array is " << r << std::endl;\r
- while( r.getKind() == kind::STORE ){\r
- Node i = fm->getUsedRepresentative( r[1] );\r
- Node e = fm->getUsedRepresentative( r[2] );\r
- d.addEntry(fm, mkArrayCond(i), e );\r
- r = r[0];\r
- }\r
- Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));\r
- bool success = false;\r
- if( r.getKind() == kind::STORE_ALL ){\r
- ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();\r
- Node defaultValue = Node::fromExpr(storeAll.getExpr());\r
- defaultValue = fm->getUsedRepresentative( defaultValue, true );\r
- if( !defaultValue.isNull() ){\r
- d.addEntry(fm, defC, defaultValue);\r
- success = true;\r
- }\r
- }\r
- if( !success ){\r
- Trace("fmc-debug") << "Can't process base array " << r << std::endl;\r
- //can't process this array\r
- d.reset();\r
- d.addEntry(fm, defC, Node::null());\r
- }\r
- }\r
- else if( n.getNumChildren()==0 ){\r
- Node r = n;\r
- if( !n.isConst() ){\r
- if( !fm->hasTerm(n) ){\r
- r = getSomeDomainElement(fm, n.getType() );\r
- }\r
- r = fm->getUsedRepresentative( r );\r
- }\r
- Trace("fmc-debug") << "Add constant entry..." << std::endl;\r
- d.addEntry(fm, mkCondDefault(fm, f), r);\r
- }\r
- else{\r
- std::vector< int > var_ch;\r
- std::vector< Def > children;\r
- for( int i=0; i<(int)n.getNumChildren(); i++) {\r
- Def dc;\r
- doCheck(fm, f, dc, n[i]);\r
- children.push_back(dc);\r
- if( n[i].getKind() == kind::BOUND_VARIABLE ){\r
- var_ch.push_back(i);\r
- }\r
- }\r
-\r
- if( n.getKind()==APPLY_UF ){\r
- Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;\r
- //uninterpreted compose\r
- doUninterpretedCompose( fm, f, d, n.getOperator(), children );\r
- } else if( n.getKind()==SELECT ){\r
- Trace("fmc-debug") << "Do select compose " << n << std::endl;\r
- std::vector< Def > children2;\r
- children2.push_back( children[1] );\r
- std::vector< Node > cond;\r
- mkCondDefaultVec(fm, f, cond);\r
- std::vector< Node > val;\r
- doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );\r
- } else {\r
- if( !var_ch.empty() ){\r
- if( n.getKind()==EQUAL ){\r
- if( var_ch.size()==2 ){\r
- Trace("fmc-debug") << "Do variable equality " << n << std::endl;\r
- doVariableEquality( fm, f, d, n );\r
- }else{\r
- Trace("fmc-debug") << "Do variable relation " << n << std::endl;\r
- doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] );\r
- }\r
- }else{\r
- Trace("fmc-warn") << "Don't know how to check " << n << std::endl;\r
- d.addEntry(fm, mkCondDefault(fm, f), Node::null());\r
- }\r
- }else{\r
- Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;\r
- std::vector< Node > cond;\r
- mkCondDefaultVec(fm, f, cond);\r
- std::vector< Node > val;\r
- //interpreted compose\r
- doInterpretedCompose( fm, f, d, n, children, 0, cond, val );\r
- }\r
- }\r
- Trace("fmc-debug") << "Simplify the definition..." << std::endl;\r
- d.debugPrint("fmc-debug", Node::null(), this);\r
- d.simplify(this, fm);\r
- Trace("fmc-debug") << "Done simplifying" << std::endl;\r
- }\r
- Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;\r
- d.debugPrint("fmc-debug", Node::null(), this);\r
- Trace("fmc-debug") << std::endl;\r
-}\r
-\r
-void FullModelChecker::doNegate( Def & dc ) {\r
- for (unsigned i=0; i<dc.d_cond.size(); i++) {\r
- if (!dc.d_value[i].isNull()) {\r
- dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;\r
- }\r
- }\r
-}\r
-\r
-void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) {\r
- std::vector<Node> cond;\r
- mkCondDefaultVec(fm, f, cond);\r
- if (eq[0]==eq[1]){\r
- d.addEntry(fm, mkCond(cond), d_true);\r
- }else{\r
- TypeNode tn = eq[0].getType();\r
- if( tn.isSort() ){\r
- int j = getVariableId(f, eq[0]);\r
- int k = getVariableId(f, eq[1]);\r
- if( !fm->d_rep_set.hasType( tn ) ){\r
- getSomeDomainElement( fm, tn ); //to verify the type is initialized\r
- }\r
- for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {\r
- Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );\r
- cond[j+1] = r;\r
- cond[k+1] = r;\r
- d.addEntry( fm, mkCond(cond), d_true);\r
- }\r
- d.addEntry( fm, mkCondDefault(fm, f), d_false);\r
- }else{\r
- d.addEntry( fm, mkCondDefault(fm, f), Node::null());\r
- }\r
- }\r
-}\r
-\r
-void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {\r
- int j = getVariableId(f, v);\r
- for (unsigned i=0; i<dc.d_cond.size(); i++) {\r
- Node val = dc.d_value[i];\r
- if( val.isNull() ){\r
- d.addEntry( fm, dc.d_cond[i], val);\r
- }else{\r
- if( dc.d_cond[i][j]!=val ){\r
- if (fm->isStar(dc.d_cond[i][j])) {\r
- std::vector<Node> cond;\r
- mkCondVec(dc.d_cond[i],cond);\r
- cond[j+1] = val;\r
- d.addEntry(fm, mkCond(cond), d_true);\r
- cond[j+1] = fm->getStar(val.getType());\r
- d.addEntry(fm, mkCond(cond), d_false);\r
- }else{\r
- d.addEntry( fm, dc.d_cond[i], d_false);\r
- }\r
- }else{\r
- d.addEntry( fm, dc.d_cond[i], d_true);\r
- }\r
- }\r
- }\r
-}\r
-\r
-void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {\r
- Trace("fmc-uf-debug") << "Definition : " << std::endl;\r
- fm->d_models[op]->debugPrint("fmc-uf-debug", op, this);\r
- Trace("fmc-uf-debug") << std::endl;\r
-\r
- std::vector< Node > cond;\r
- mkCondDefaultVec(fm, f, cond);\r
- std::vector< Node > val;\r
- doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val);\r
-}\r
-\r
-void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,\r
- Def & df, std::vector< Def > & dc, int index,\r
- std::vector< Node > & cond, std::vector<Node> & val ) {\r
- Trace("fmc-uf-process") << "process at " << index << std::endl;\r
- for( unsigned i=1; i<cond.size(); i++) {\r
- debugPrint("fmc-uf-process", cond[i], true);\r
- Trace("fmc-uf-process") << " ";\r
- }\r
- Trace("fmc-uf-process") << std::endl;\r
- if (index==(int)dc.size()) {\r
- //we have an entry, now do actual compose\r
- std::map< int, Node > entries;\r
- doUninterpretedCompose2( fm, f, entries, 0, cond, val, df.d_et);\r
- if( entries.empty() ){\r
- d.addEntry(fm, mkCond(cond), Node::null());\r
- }else{\r
- //add them to the definition\r
- for( unsigned e=0; e<df.d_cond.size(); e++ ){\r
- if ( entries.find(e)!=entries.end() ){\r
- Trace("fmf-uf-process-debug") << "Add entry..." << std::endl;\r
- d.addEntry(fm, entries[e], df.d_value[e] );\r
- Trace("fmf-uf-process-debug") << "Done add entry." << std::endl;\r
- }\r
- }\r
- }\r
- }else{\r
- for (unsigned i=0; i<dc[index].d_cond.size(); i++) {\r
- if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {\r
- std::vector< Node > new_cond;\r
- new_cond.insert(new_cond.end(), cond.begin(), cond.end());\r
- if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){\r
- Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;\r
- val.push_back(dc[index].d_value[i]);\r
- doUninterpretedCompose(fm, f, d, df, dc, index+1, new_cond, val);\r
- val.pop_back();\r
- }else{\r
- Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;\r
- }\r
- }\r
- }\r
- }\r
-}\r
-\r
-void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,\r
- std::map< int, Node > & entries, int index,\r
- std::vector< Node > & cond, std::vector< Node > & val,\r
- EntryTrie & curr ) {\r
- Trace("fmc-uf-process") << "compose " << index << std::endl;\r
- for( unsigned i=1; i<cond.size(); i++) {\r
- debugPrint("fmc-uf-process", cond[i], true);\r
- Trace("fmc-uf-process") << " ";\r
- }\r
- Trace("fmc-uf-process") << std::endl;\r
- if (index==(int)val.size()) {\r
- Node c = mkCond(cond);\r
- Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl;\r
- entries[curr.d_data] = c;\r
- }else{\r
- Node v = val[index];\r
- bool bind_var = false;\r
- if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){\r
- int j = getVariableId(f, v);\r
- Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;\r
- if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) {\r
- v = cond[j+1];\r
- }else{\r
- bind_var = true;\r
- }\r
- }\r
- if (bind_var) {\r
- Trace("fmc-uf-process") << "bind variable..." << std::endl;\r
- int j = getVariableId(f, v);\r
- if( fm->isStar(cond[j+1]) ){\r
- for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {\r
- cond[j+1] = it->first;\r
- doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
- }\r
- cond[j+1] = fm->getStar(v.getType());\r
- }else{\r
- Node orig = cond[j+1];\r
- for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {\r
- Node nw = doIntervalMeet( fm, it->first, orig );\r
- if( !nw.isNull() ){\r
- cond[j+1] = nw;\r
- doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
- }\r
- }\r
- cond[j+1] = orig;\r
- }\r
- }else{\r
- if( !v.isNull() ){\r
- if( options::fmfFmcInterval() && v.getType().isInteger() ){\r
- for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {\r
- if( fm->isInRange( v, it->first ) ){\r
- doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
- }\r
- }\r
- }else{\r
- if (curr.d_child.find(v)!=curr.d_child.end()) {\r
- Trace("fmc-uf-process") << "follow value..." << std::endl;\r
- doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);\r
- }\r
- Node st = fm->getStarElement(v.getType());\r
- if (curr.d_child.find(st)!=curr.d_child.end()) {\r
- Trace("fmc-uf-process") << "follow star..." << std::endl;\r
- doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);\r
- }\r
- }\r
- }\r
- }\r
- }\r
-}\r
-\r
-void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,\r
- std::vector< Def > & dc, int index,\r
- std::vector< Node > & cond, std::vector<Node> & val ) {\r
- if ( index==(int)dc.size() ){\r
- Node c = mkCond(cond);\r
- Node v = evaluateInterpreted(n, val);\r
- d.addEntry(fm, c, v);\r
- }\r
- else {\r
- TypeNode vtn = n.getType();\r
- for (unsigned i=0; i<dc[index].d_cond.size(); i++) {\r
- if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {\r
- std::vector< Node > new_cond;\r
- new_cond.insert(new_cond.end(), cond.begin(), cond.end());\r
- if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){\r
- bool process = true;\r
- if (vtn.isBoolean()) {\r
- //short circuit\r
- if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||\r
- (n.getKind()==AND && dc[index].d_value[i]==d_false) ){\r
- Node c = mkCond(new_cond);\r
- d.addEntry(fm, c, dc[index].d_value[i]);\r
- process = false;\r
- }\r
- }\r
- if (process) {\r
- val.push_back(dc[index].d_value[i]);\r
- doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val);\r
- val.pop_back();\r
- }\r
- }\r
- }\r
- }\r
- }\r
-}\r
-\r
-int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {\r
- Trace("fmc-debug2") << "isCompat " << c << std::endl;\r
- Assert(cond.size()==c.getNumChildren()+1);\r
- for (unsigned i=1; i<cond.size(); i++) {\r
- if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){\r
- Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );\r
- if( iv.isNull() ){\r
- return 0;\r
- }\r
- }else{\r
- if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {\r
- return 0;\r
- }\r
- }\r
- }\r
- return 1;\r
-}\r
-\r
-bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {\r
- Trace("fmc-debug2") << "doMeet " << c << std::endl;\r
- Assert(cond.size()==c.getNumChildren()+1);\r
- for (unsigned i=1; i<cond.size(); i++) {\r
- if( cond[i]!=c[i-1] ) {\r
- if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){\r
- Node iv = doIntervalMeet( fm, cond[i], c[i-1] );\r
- if( !iv.isNull() ){\r
- cond[i] = iv;\r
- }else{\r
- return false;\r
- }\r
- }else{\r
- if( fm->isStar(cond[i]) ){\r
- cond[i] = c[i-1];\r
- }else if( !fm->isStar(c[i-1]) ){\r
- return false;\r
- }\r
- }\r
- }\r
- }\r
- return true;\r
-}\r
-\r
-Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {\r
- if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){\r
- std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;\r
- exit( 0 );\r
- }\r
- Node b[2];\r
- for( unsigned j=0; j<2; j++ ){\r
- Node b1 = i1[j];\r
- Node b2 = i2[j];\r
- if( fm->isStar( b1 ) ){\r
- b[j] = b2;\r
- }else if( fm->isStar( b2 ) ){\r
- b[j] = b1;\r
- }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){\r
- b[j] = j==0 ? b2 : b1;\r
- }else{\r
- b[j] = j==0 ? b1 : b2;\r
- }\r
- }\r
- if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){\r
- return mk ? fm->getInterval( b[0], b[1] ) : i1;\r
- }else{\r
- return Node::null();\r
- }\r
-}\r
-\r
-Node FullModelChecker::mkCond( std::vector< Node > & cond ) {\r
- return NodeManager::currentNM()->mkNode(APPLY_UF, cond);\r
-}\r
-\r
-Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {\r
- std::vector< Node > cond;\r
- mkCondDefaultVec(fm, f, cond);\r
- return mkCond(cond);\r
-}\r
-\r
-void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {\r
- Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl;\r
- //get function symbol for f\r
- cond.push_back(d_quant_cond[f]);\r
- for (unsigned i=0; i<f[0].getNumChildren(); i++) {\r
- Node ts = fm->getStarElement( f[0][i].getType() );\r
- cond.push_back(ts);\r
- }\r
-}\r
-\r
-void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {\r
- cond.push_back(n.getOperator());\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- cond.push_back( n[i] );\r
- }\r
-}\r
-\r
-Node FullModelChecker::mkArrayCond( Node a ) {\r
- if( d_array_term_cond.find(a)==d_array_term_cond.end() ){\r
- if( d_array_cond.find(a.getType())==d_array_cond.end() ){\r
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() );\r
- Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );\r
- d_array_cond[a.getType()] = op;\r
- }\r
- std::vector< Node > cond;\r
- cond.push_back(d_array_cond[a.getType()]);\r
- cond.push_back(a);\r
- d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond );\r
- }\r
- return d_array_term_cond[a];\r
-}\r
-\r
-Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {\r
- if( n.getKind()==EQUAL ){\r
- if (!vals[0].isNull() && !vals[1].isNull()) {\r
- return vals[0]==vals[1] ? d_true : d_false;\r
- }else{\r
- return Node::null();\r
- }\r
- }else if( n.getKind()==ITE ){\r
- if( vals[0]==d_true ){\r
- return vals[1];\r
- }else if( vals[0]==d_false ){\r
- return vals[2];\r
- }else{\r
- return vals[1]==vals[2] ? vals[1] : Node::null();\r
- }\r
- }else if( n.getKind()==AND || n.getKind()==OR ){\r
- bool isNull = false;\r
- for (unsigned i=0; i<vals.size(); i++) {\r
- if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) {\r
- return vals[i];\r
- }else if( vals[i].isNull() ){\r
- isNull = true;\r
- }\r
- }\r
- return isNull ? Node::null() : vals[0];\r
- }else{\r
- std::vector<Node> children;\r
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){\r
- children.push_back( n.getOperator() );\r
- }\r
- for (unsigned i=0; i<vals.size(); i++) {\r
- if( vals[i].isNull() ){\r
- return Node::null();\r
- }else{\r
- children.push_back( vals[i] );\r
- }\r
- }\r
- Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children);\r
- Trace("fmc-eval") << "Evaluate " << nc << " to ";\r
- nc = Rewriter::rewrite(nc);\r
- Trace("fmc-eval") << nc << std::endl;\r
- return nc;\r
- }\r
-}\r
-\r
-Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) {\r
- bool addRepId = !fm->d_rep_set.hasType( tn );\r
- Node de = fm->getSomeDomainElement(tn);\r
- if( addRepId ){\r
- d_rep_ids[tn][de] = 0;\r
- }\r
- return de;\r
-}\r
-\r
-Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {\r
- return fm->getFunctionValue(op, argPrefix);\r
-}\r
-\r
-\r
-bool FullModelChecker::useSimpleModels() {\r
- return options::fmfFmcSimple();\r
-}\r
-\r
-void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,\r
- std::map< int, std::map< int, Node > >& changed_vals ) {\r
- if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){\r
- makeIntervalModel2( fm, op, indices, 0, changed_vals );\r
- }else{\r
- TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();\r
- if( tn.isInteger() ){\r
- makeIntervalModel(fm,op,indices,index+1, changed_vals );\r
- }else{\r
- std::map< Node, std::vector< int > > new_indices;\r
- for( unsigned i=0; i<indices.size(); i++ ){\r
- Node v = fm->d_models[op]->d_cond[indices[i]][index];\r
- new_indices[v].push_back( indices[i] );\r
- }\r
-\r
- for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){\r
- makeIntervalModel( fm, op, it->second, index+1, changed_vals );\r
- }\r
- }\r
- }\r
-}\r
-\r
-void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,\r
- std::map< int, std::map< int, Node > >& changed_vals ) {\r
- Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : ";\r
- for( unsigned i=0; i<indices.size(); i++ ){\r
- Debug("fmc-interval-model-debug") << indices[i] << " ";\r
- }\r
- Debug("fmc-interval-model-debug") << std::endl;\r
-\r
- if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){\r
- TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();\r
- if( tn.isInteger() ){\r
- std::map< Node, std::vector< int > > new_indices;\r
- for( unsigned i=0; i<indices.size(); i++ ){\r
- Node v = fm->d_models[op]->d_cond[indices[i]][index];\r
- new_indices[v].push_back( indices[i] );\r
- if( !v.isConst() ){\r
- Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl;\r
- Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl;\r
- }\r
- }\r
-\r
- std::vector< Node > values;\r
- for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){\r
- makeIntervalModel2( fm, op, it->second, index+1, changed_vals );\r
- values.push_back( it->first );\r
- }\r
-\r
- if( tn.isInteger() ){\r
- //sort values by size\r
- ConstRationalSort crs;\r
- std::vector< int > sindices;\r
- for( unsigned i=0; i<values.size(); i++ ){\r
- sindices.push_back( (int)i );\r
- crs.d_terms.push_back( values[i] );\r
- }\r
- std::sort( sindices.begin(), sindices.end(), crs );\r
-\r
- Node ub = fm->getStar( tn );\r
- for( int i=(int)(sindices.size()-1); i>=0; i-- ){\r
- Node lb = fm->getStar( tn );\r
- if( i>0 ){\r
- lb = values[sindices[i]];\r
- }\r
- Node interval = fm->getInterval( lb, ub );\r
- for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){\r
- Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl;\r
- changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;\r
- }\r
- ub = lb;\r
- }\r
- }\r
- }else{\r
- makeIntervalModel2( fm, op, indices, index+1, changed_vals );\r
- }\r
- }\r
-}
\ No newline at end of file
+
+/********************* */
+/*! \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 << 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 ) ){
+ d_addedLemmas++;
+ }else{
+ //this can happen if evaluation is unknown
+ //might try it next effort level
+ d_star_insts[f].push_back(i);
+ }
+ }else{
+ //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 = r[0];
+ }
+ Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));
+ bool success = false;
+ if( r.getKind() == kind::STORE_ALL ){
+ ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();
+ Node defaultValue = Node::fromExpr(storeAll.getExpr());
+ defaultValue = fm->getUsedRepresentative( defaultValue, true );
+ if( !defaultValue.isNull() ){
+ d.addEntry(fm, defC, defaultValue);
+ success = true;
+ }
+ }
+ if( !success ){
+ 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-debug2") << "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-debug2") << "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->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 );
+ }
+ }
+}
projects / cvc5.git / commitdiff