diff options
29 files changed, 2814 insertions, 2778 deletions
diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 0eca68c13..e75476e8e 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -102,3 +102,19 @@ AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main() { return 0; }])], AC_LANG_POP([C++]) CXXFLAGS="$cvc4_save_CXXFLAGS" ])# CVC4_CXX_OPTION + +# CVC4_C_OPTION(OPTION, VAR) +# -------------------------- +# Run $(CC) $(CPPFLAGS) $(CFLAGS) OPTION and see if the compiler +# likes it. If so, add OPTION to shellvar VAR. +AC_DEFUN([CVC4_C_OPTION], [ +AC_MSG_CHECKING([whether $CC supports $1]) +cvc4_save_CFLAGS="$CFLAGS" +CFLAGS="$CFLAGS $C_WERROR $1" +AC_LANG_PUSH([C]) +AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main() { return 0; }])], + [AC_MSG_RESULT([yes]); $2='$1'], + [AC_MSG_RESULT([no])]) +AC_LANG_POP([C]) +CFLAGS="$cvc4_save_CFLAGS" +])# CVC4_C_OPTION diff --git a/config/doxygen.cfg b/config/doxygen.cfg index f4713b616..f385fb94a 100644 --- a/config/doxygen.cfg +++ b/config/doxygen.cfg @@ -1247,7 +1247,7 @@ SEARCH_INCLUDES = YES # contain include files that are not input files but should be processed by # the preprocessor. -INCLUDE_PATH = . include $(SRCDIR)/src $(SRCDIR)/src/include +INCLUDE_PATH = . $(SRCDIR)/src $(SRCDIR)/src/include # You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard # patterns (like *.h and *.hpp) to filter out the header-files in the diff --git a/configure.ac b/configure.ac index bbec2970c..dce990c69 100644 --- a/configure.ac +++ b/configure.ac @@ -786,6 +786,9 @@ AC_DEFINE_UNQUOTED(CVC4_GCC_HAS_PB_DS_BUG, ${CVC4_GCC_HAS_PB_DS_BUG}, [Whether l AC_PROG_ANTLR CVC4_CXX_OPTION([-Werror], [WERROR]) +CVC4_C_OPTION([-Werror], [C_WERROR]) +CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED]) +CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED]) CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL]) CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE]) CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES]) @@ -1037,8 +1040,8 @@ cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS" cvc4_rlcheck_save_CFLAGS="$CFLAGS" cvc4_rlcheck_save_LDFLAGS="$LDFLAGS" CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS" -CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated" -CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions" +CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED" +CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions" LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" CVC4_CHECK_FOR_READLINE CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS" diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index cc2a7c53f..90c8a3b42 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -142,7 +142,7 @@ endif endif nodist_java_libcvc4jni_la_SOURCES = java.cpp -java_libcvc4jni_la_CXXFLAGS = @FNO_STRICT_ALIASING@ @WNO_UNUSED_VARIABLE@ @WNO_UNINITIALIZED@ +java_libcvc4jni_la_CXXFLAGS = -Wno-all @FNO_STRICT_ALIASING@ @WNO_UNUSED_VARIABLE@ @WNO_UNINITIALIZED@ nodist_csharp_CVC4_la_SOURCES = csharp.cpp nodist_perl_CVC4_la_SOURCES = perl.cpp nodist_php_CVC4_la_SOURCES = php.cpp @@ -171,8 +171,8 @@ MOSTLYCLEANFILES = \ $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \ CVC4.jar -java_libcvc4jni_la-java.lo java.lo: java.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) $(java_libcvc4jni_la_CXXFLAGS) -o $@ $< +#java_libcvc4jni_la-java.lo java.lo: java.cpp +# $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) $(java_libcvc4jni_la_CXXFLAGS) -o $@ $< CVC4.jar: java.cpp $(AM_V_GEN) \ (cd java && \ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 8486e8ec3..41813abde 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -270,6 +270,13 @@ inline void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) { toStream(out, n.d_nv); } +// The reinterpret_cast of d_children to various constant payload types +// in deleteNodeValueConstant(), below, can flag a "strict aliasing" +// warning; it should actually be okay, because we never access the +// embedded constant as a NodeValue* child, and never access an embedded +// NodeValue* child as a constant. +#pragma GCC diagnostic ignored "-Wstrict-aliasing" + /** * Cleanup to be performed when a NodeValue zombie is collected, and * it has CONSTANT metakind. This calls the destructor for the underlying @@ -289,6 +296,9 @@ ${metakind_constDeleters} } } +// re-enable the strict-aliasing warning +# pragma GCC diagnostic warning "-Wstrict-aliasing" + inline unsigned getLowerBoundForKind(::CVC4::Kind k) { static const unsigned lbs[] = { 0, /* NULL_EXPR */ @@ -334,7 +344,7 @@ ${metakind_operatorKinds} }/* CVC4::kind namespace */ -#line 338 "${template}" +#line 348 "${template}" namespace theory { diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 229c25597..d97d11364 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -576,7 +576,7 @@ std::vector<std::string> Options::suggestCommandLineOptions(const std::string& o static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 590 "${template}" +#line 580 "${template}" NULL };/* smtOptions[] */ @@ -598,7 +598,7 @@ SExpr Options::getOptions() const throw() { ${all_modules_get_options} -#line 612 "${template}" +#line 602 "${template}" return SExpr(opts); } diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 7c5d48c1c..b7066dd7e 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable $(WNO_CONVERSION_NULL) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable $(WNO_UNINITIALIZED) $(WNO_CONVERSION_NULL) # Compile generated C files using C++ compiler CC=$(CXX) diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index ee72d1949..dea78acf7 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file arith_priority_queue.cpp +/*! \file error_set.cpp ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters + ** 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 ** diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index c5174a86a..d1b692cb4 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file arith_priority_queue.h +/*! \file error_set.h ** \verbatim - ** Original author: taking + ** Original author: Tim King ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters + ** 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 ** diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 47aac4370..d17dd588f 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -178,7 +178,7 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) { } -/** +/* * Asserts the clauses corresponding to the atom to the Sat Solver * by turning on the marker literal (i.e. setting it to false) * @param node the atom to be asserted @@ -444,6 +444,8 @@ bool Bitblaster::hasValue(TNode a) { * or null if the value is completely unassigned. * * @param a + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them * * @return */ diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 83efc05b0..6fab0369c 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -152,13 +152,14 @@ public: * Adds a constant value for each bit-blasted variable in the model. * * @param m the model + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them */ void collectModelInfo(TheoryModel* m, bool fullModel); /** * Stores the variable (or non-bv term) and its corresponding bits. * * @param var - * @param bits */ void storeVariable(TNode var) { d_variables.insert(var); diff --git a/src/theory/idl/options b/src/theory/idl/options index 0048353b9..c1c9edcef 100644 --- a/src/theory/idl/options +++ b/src/theory/idl/options @@ -6,5 +6,7 @@ module IDL "theory/idl/options.h" Idl option idlRewriteEq --enable-idl-rewrite-equalities/--disable-idl-rewrite-equalities bool :default false :read-write + enable rewriting equalities into two inequalities in IDL solver (default is disabled) +/disable rewriting equalities into two inequalities in IDL solver (default is disabled) endmodule diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index d893a9ff2..13e075265 100755 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -1,366 +1,366 @@ -/********************* */
-/*! \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));
-}
\ 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)); +} diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 96d2a3d20..27d5b7569 100755 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -1,126 +1,126 @@ -/********************* */
-/*! \file bounded_integers.h
-** \verbatim
-** Original author: Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013 New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief This class manages integer bounds for quantifiers
-**/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__BOUNDED_INTEGERS_H
-#define __CVC4__BOUNDED_INTEGERS_H
-
-
-#include "theory/quantifiers_engine.h"
-
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "context/cdchunk_list.h"
-
-namespace CVC4 {
-namespace theory {
-
-class RepSetIterator;
-
-namespace quantifiers {
-
-
-class BoundedIntegers : public QuantifiersModule
-{
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
-private:
- //for determining bounds
- bool isBound( Node f, Node v );
- bool hasNonBoundVar( Node f, Node b );
- std::map< Node, std::map< Node, Node > > d_bounds[2];
- std::map< Node, std::vector< Node > > d_set;
- std::map< Node, std::vector< int > > d_set_nums;
- std::map< Node, std::map< Node, Node > > d_range;
- std::map< Node, std::map< Node, Node > > d_nground_range;
- void hasFreeVar( Node f, Node n );
- void process( Node f, Node n, bool pol,
- std::map< int, std::map< Node, Node > >& bound_lit_map,
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map );
- void processLiteral( Node f, Node lit, bool pol,
- std::map< int, std::map< Node, Node > >& bound_lit_map,
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map );
- std::vector< Node > d_bound_quants;
-private:
- class RangeModel {
- private:
- BoundedIntegers * d_bi;
- void allocateRange();
- public:
- RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi),
- d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {}
- Node d_range;
- int d_curr_max;
- std::map< int, Node > d_range_literal;
- std::map< Node, bool > d_lit_to_pol;
- std::map< Node, int > d_lit_to_range;
- NodeBoolMap d_range_assertions;
- context::CDO< bool > d_has_range;
- context::CDO< int > d_curr_range;
- void initialize();
- void assertNode(Node n);
- Node getNextDecisionRequest();
- };
-private:
- //information for minimizing ranges
- std::vector< Node > d_ranges;
- //map to range model objects
- std::map< Node, RangeModel * > d_rms;
- //literal to range
- std::map< Node, std::vector< Node > > d_lit_to_ranges;
- //list of currently asserted arithmetic literals
- NodeBoolMap d_assertions;
-private:
- //class to store whether bounding lemmas have been added
- class BoundInstTrie
- {
- public:
- std::map< Node, BoundInstTrie > d_children;
- bool hasInstantiated( std::vector< Node > & vals, int index = 0, bool madeNew = false ){
- if( index>=(int)vals.size() ){
- return !madeNew;
- }else{
- Node n = vals[index];
- if( d_children.find(n)==d_children.end() ){
- madeNew = true;
- }
- return d_children[n].hasInstantiated(vals,index+1,madeNew);
- }
- }
- };
- std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
-private:
- void addLiteralFromRange( Node lit, Node r );
-public:
- BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
-
- void check( Theory::Effort e );
- void registerQuantifier( Node f );
- void assertNode( Node n );
- Node getNextDecisionRequest();
- bool isBoundVar( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); }
- unsigned getNumBoundVars( Node f ) { return d_set[f].size(); }
- Node getBoundVar( Node f, int i ) { return d_set[f][i]; }
- int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; }
- Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }
- Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }
- void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
- bool isGroundRange(Node f, Node v);
-};
-
-}
-}
-}
-
-#endif
\ No newline at end of file +/********************* */ +/*! \file bounded_integers.h +** \verbatim +** Original author: Andrew Reynolds +** This file is part of the CVC4 project. +** Copyright (c) 2009-2013 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief This class manages integer bounds for quantifiers +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BOUNDED_INTEGERS_H +#define __CVC4__BOUNDED_INTEGERS_H + + +#include "theory/quantifiers_engine.h" + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.h" + +namespace CVC4 { +namespace theory { + +class RepSetIterator; + +namespace quantifiers { + + +class BoundedIntegers : public QuantifiersModule +{ + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; +private: + //for determining bounds + bool isBound( Node f, Node v ); + bool hasNonBoundVar( Node f, Node b ); + std::map< Node, std::map< Node, Node > > d_bounds[2]; + std::map< Node, std::vector< Node > > d_set; + std::map< Node, std::vector< int > > d_set_nums; + std::map< Node, std::map< Node, Node > > d_range; + std::map< Node, std::map< Node, Node > > d_nground_range; + void hasFreeVar( Node f, Node n ); + void process( Node f, Node n, bool pol, + std::map< int, std::map< Node, Node > >& bound_lit_map, + std::map< int, std::map< Node, bool > >& bound_lit_pol_map ); + void processLiteral( Node f, Node lit, bool pol, + std::map< int, std::map< Node, Node > >& bound_lit_map, + std::map< int, std::map< Node, bool > >& bound_lit_pol_map ); + std::vector< Node > d_bound_quants; +private: + class RangeModel { + private: + BoundedIntegers * d_bi; + void allocateRange(); + public: + RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi), + d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {} + Node d_range; + int d_curr_max; + std::map< int, Node > d_range_literal; + std::map< Node, bool > d_lit_to_pol; + std::map< Node, int > d_lit_to_range; + NodeBoolMap d_range_assertions; + context::CDO< bool > d_has_range; + context::CDO< int > d_curr_range; + void initialize(); + void assertNode(Node n); + Node getNextDecisionRequest(); + }; +private: + //information for minimizing ranges + std::vector< Node > d_ranges; + //map to range model objects + std::map< Node, RangeModel * > d_rms; + //literal to range + std::map< Node, std::vector< Node > > d_lit_to_ranges; + //list of currently asserted arithmetic literals + NodeBoolMap d_assertions; +private: + //class to store whether bounding lemmas have been added + class BoundInstTrie + { + public: + std::map< Node, BoundInstTrie > d_children; + bool hasInstantiated( std::vector< Node > & vals, int index = 0, bool madeNew = false ){ + if( index>=(int)vals.size() ){ + return !madeNew; + }else{ + Node n = vals[index]; + if( d_children.find(n)==d_children.end() ){ + madeNew = true; + } + return d_children[n].hasInstantiated(vals,index+1,madeNew); + } + } + }; + std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; +private: + void addLiteralFromRange( Node lit, Node r ); +public: + BoundedIntegers( context::Context* c, QuantifiersEngine* qe ); + + void check( Theory::Effort e ); + void registerQuantifier( Node f ); + void assertNode( Node n ); + Node getNextDecisionRequest(); + bool isBoundVar( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); } + unsigned getNumBoundVars( Node f ) { return d_set[f].size(); } + Node getBoundVar( Node f, int i ) { return d_set[f][i]; } + int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; } + Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; } + Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; } + void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); + bool isGroundRange(Node f, Node v); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index e20f8c8e8..42b49cf01 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -211,4 +211,4 @@ Node CandidateGeneratorQEAll::getNextCandidate() { } } return Node::null(); -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp index 27fcebccf..ebfb55f08 100755 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ b/src/theory/quantifiers/first_order_reasoning.cpp @@ -1,171 +1,171 @@ -/********************* */
-/*! \file first_order_reasoning.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief first order reasoning module
- **
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/first_order_reasoning.h"
-#include "theory/rewriter.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace std;
-
-namespace CVC4 {
-
-
-void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){
- if( n.getKind()==FORALL ){
- collectLits( n[1], lits );
- }else if( n.getKind()==OR ){
- for(unsigned j=0; j<n.getNumChildren(); j++) {
- collectLits(n[j], lits );
- }
- }else{
- lits.push_back( n );
- }
-}
-
-void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){
- for( unsigned i=0; i<assertions.size(); i++) {
- Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl;
- }
-
- //process all assertions
- int num_processed;
- int num_true = 0;
- int num_rounds = 0;
- do {
- num_processed = 0;
- for( unsigned i=0; i<assertions.size(); i++ ){
- if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){
- std::vector< Node > fo_lits;
- collectLits( assertions[i], fo_lits );
- Node unitLit = process( assertions[i], fo_lits );
- if( !unitLit.isNull() ){
- Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl;
- bool pol = unitLit.getKind()!=NOT;
- unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit;
- if( unitLit.getKind()==EQUAL ){
-
- }else if( unitLit.getKind()==APPLY_UF ){
- //make sure all are unique vars;
- bool success = true;
- std::vector< Node > unique_vars;
- for( unsigned j=0; j<unitLit.getNumChildren(); j++) {
- if( unitLit[j].getKind()==BOUND_VARIABLE ){
- if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){
- unique_vars.push_back( unitLit[j] );
- }else{
- success = false;
- break;
- }
- }else{
- success = false;
- break;
- }
- }
- if( success ){
- d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol);
- Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl;
- Trace("fo-rsn") << " from : " << assertions[i] << std::endl;
- d_assertion_true[assertions[i]] = true;
- num_processed++;
- }
- }else if( unitLit.getKind()==VARIABLE ){
- d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol);
- Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl;
- Trace("fo-rsn") << " from : " << assertions[i] << std::endl;
- d_assertion_true[assertions[i]] = true;
- num_processed++;
- }
- }
- if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){
- num_true++;
- }
- }
- }
- num_rounds++;
- }while( num_processed>0 );
- Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl;
- for( unsigned i=0; i<assertions.size(); i++ ){
- assertions[i] = theory::Rewriter::rewrite( simplify( assertions[i] ) );
- }
-}
-
-Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) {
- int index = -1;
- for( unsigned i=0; i<lits.size(); i++) {
- bool pol = lits[i].getKind()!=NOT;
- Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i];
- Node litDef;
- if( n.getKind()==APPLY_UF ){
- if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
- litDef = d_const_def[n.getOperator()];
- }
- }else if( n.getKind()==VARIABLE ){
- if( d_const_def.find(n)!=d_const_def.end() ){
- litDef = d_const_def[n];
- }
- }
- if( !litDef.isNull() ){
- Node poln = NodeManager::currentNM()->mkConst( pol );
- if( litDef==poln ){
- Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl;
- d_assertion_true[a] = true;
- return Node::null();
- }
- }
- if( litDef.isNull() ){
- if( index==-1 ){
- //store undefined index
- index = i;
- }else{
- //two undefined, return null
- return Node::null();
- }
- }
- }
- if( index!=-1 ){
- return lits[index];
- }else{
- return Node::null();
- }
-}
-
-Node FirstOrderPropagation::simplify( Node n ) {
- if( n.getKind()==VARIABLE ){
- if( d_const_def.find(n)!=d_const_def.end() ){
- return d_const_def[n];
- }
- }else if( n.getKind()==APPLY_UF ){
- if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
- return d_const_def[n.getOperator()];
- }
- }
- if( n.getNumChildren()==0 ){
- return n;
- }else{
- std::vector< Node > children;
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- for(unsigned i=0; i<n.getNumChildren(); i++) {
- children.push_back( simplify(n[i]) );
- }
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
-}
-
-}
+/********************* */ +/*! \file first_order_reasoning.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief first order reasoning module + ** + **/ + +#include <vector> + +#include "theory/quantifiers/first_order_reasoning.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { + + +void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){ + if( n.getKind()==FORALL ){ + collectLits( n[1], lits ); + }else if( n.getKind()==OR ){ + for(unsigned j=0; j<n.getNumChildren(); j++) { + collectLits(n[j], lits ); + } + }else{ + lits.push_back( n ); + } +} + +void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){ + for( unsigned i=0; i<assertions.size(); i++) { + Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl; + } + + //process all assertions + int num_processed; + int num_true = 0; + int num_rounds = 0; + do { + num_processed = 0; + for( unsigned i=0; i<assertions.size(); i++ ){ + if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){ + std::vector< Node > fo_lits; + collectLits( assertions[i], fo_lits ); + Node unitLit = process( assertions[i], fo_lits ); + if( !unitLit.isNull() ){ + Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl; + bool pol = unitLit.getKind()!=NOT; + unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit; + if( unitLit.getKind()==EQUAL ){ + + }else if( unitLit.getKind()==APPLY_UF ){ + //make sure all are unique vars; + bool success = true; + std::vector< Node > unique_vars; + for( unsigned j=0; j<unitLit.getNumChildren(); j++) { + if( unitLit[j].getKind()==BOUND_VARIABLE ){ + if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){ + unique_vars.push_back( unitLit[j] ); + }else{ + success = false; + break; + } + }else{ + success = false; + break; + } + } + if( success ){ + d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol); + Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl; + Trace("fo-rsn") << " from : " << assertions[i] << std::endl; + d_assertion_true[assertions[i]] = true; + num_processed++; + } + }else if( unitLit.getKind()==VARIABLE ){ + d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol); + Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl; + Trace("fo-rsn") << " from : " << assertions[i] << std::endl; + d_assertion_true[assertions[i]] = true; + num_processed++; + } + } + if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){ + num_true++; + } + } + } + num_rounds++; + }while( num_processed>0 ); + Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl; + for( unsigned i=0; i<assertions.size(); i++ ){ + assertions[i] = theory::Rewriter::rewrite( simplify( assertions[i] ) ); + } +} + +Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) { + int index = -1; + for( unsigned i=0; i<lits.size(); i++) { + bool pol = lits[i].getKind()!=NOT; + Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i]; + Node litDef; + if( n.getKind()==APPLY_UF ){ + if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ + litDef = d_const_def[n.getOperator()]; + } + }else if( n.getKind()==VARIABLE ){ + if( d_const_def.find(n)!=d_const_def.end() ){ + litDef = d_const_def[n]; + } + } + if( !litDef.isNull() ){ + Node poln = NodeManager::currentNM()->mkConst( pol ); + if( litDef==poln ){ + Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl; + d_assertion_true[a] = true; + return Node::null(); + } + } + if( litDef.isNull() ){ + if( index==-1 ){ + //store undefined index + index = i; + }else{ + //two undefined, return null + return Node::null(); + } + } + } + if( index!=-1 ){ + return lits[index]; + }else{ + return Node::null(); + } +} + +Node FirstOrderPropagation::simplify( Node n ) { + if( n.getKind()==VARIABLE ){ + if( d_const_def.find(n)!=d_const_def.end() ){ + return d_const_def[n]; + } + }else if( n.getKind()==APPLY_UF ){ + if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ + return d_const_def[n.getOperator()]; + } + } + if( n.getNumChildren()==0 ){ + return n; + }else{ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for(unsigned i=0; i<n.getNumChildren(); i++) { + children.push_back( simplify(n[i]) ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + } +} + +} diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h index 0dbf23a3b..5f217050c 100755 --- a/src/theory/quantifiers/first_order_reasoning.h +++ b/src/theory/quantifiers/first_order_reasoning.h @@ -1,45 +1,45 @@ -/********************* */
-/*! \file first_order_reasoning.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Pre-process step for first-order reasoning
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__FIRST_ORDER_REASONING_H
-#define __CVC4__FIRST_ORDER_REASONING_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-
-namespace CVC4 {
-
-class FirstOrderPropagation {
-private:
- std::map< Node, Node > d_const_def;
- std::map< Node, bool > d_assertion_true;
- Node process(Node a, std::vector< Node > & lits);
- void collectLits( Node n, std::vector<Node> & lits );
- Node simplify( Node n );
-public:
- FirstOrderPropagation(){}
- ~FirstOrderPropagation(){}
-
- void simplify( std::vector< Node >& assertions );
-};
-
-}
-
-#endif
+/********************* */ +/*! \file first_order_reasoning.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process step for first-order reasoning + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__FIRST_ORDER_REASONING_H +#define __CVC4__FIRST_ORDER_REASONING_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class FirstOrderPropagation { +private: + std::map< Node, Node > d_const_def; + std::map< Node, bool > d_assertion_true; + Node process(Node a, std::vector< Node > & lits); + void collectLits( Node n, std::vector<Node> & lits ); + Node simplify( Node n ); +public: + FirstOrderPropagation(){} + ~FirstOrderPropagation(){} + + void simplify( std::vector< Node >& assertions ); +}; + +} + +#endif diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 4c168acfc..6e7986390 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -1,1398 +1,1398 @@ -
-/********************* */
-/*! \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 );
- }
- }
-}
\ 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 ); + } + } +} diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index fb810c355..93174677f 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -1,158 +1,158 @@ -/********************* */
-/*! \file full_model_check.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Full model check class
- **/
-
-#ifndef FULL_MODEL_CHECK
-#define FULL_MODEL_CHECK
-
-#include "theory/quantifiers/model_builder.h"
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-namespace fmcheck {
-
-
-class FirstOrderModelFmc;
-class FullModelChecker;
-
-class EntryTrie
-{
-private:
- int d_complete;
-public:
- EntryTrie() : d_complete(-1), d_data(-1){}
- std::map<Node,EntryTrie> d_child;
- int d_data;
- void reset() { d_data = -1; d_child.clear(); d_complete = -1; }
- void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 );
- bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );
- int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );
- void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
-
- void collectIndices(Node c, int index, std::vector< int >& indices );
- bool isComplete(FirstOrderModelFmc * m, Node c, int index);
-};
-
-
-class Def
-{
-public:
- EntryTrie d_et;
- //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative
- std::vector< Node > d_cond;
- //value is returned by FullModelChecker::getRepresentative
- std::vector< Node > d_value;
- void basic_simplify( FirstOrderModelFmc * m );
-private:
- enum {
- status_unk,
- status_redundant,
- status_non_redundant
- };
- std::vector< int > d_status;
- bool d_has_simplified;
-public:
- Def() : d_has_simplified(false){}
- void reset() {
- d_et.reset();
- d_cond.clear();
- d_value.clear();
- d_status.clear();
- d_has_simplified = false;
- }
- bool addEntry( FirstOrderModelFmc * m, Node c, Node v);
- Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst );
- int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );
- void simplify( FullModelChecker * mc, FirstOrderModelFmc * m );
- void debugPrint(const char * tr, Node op, FullModelChecker * m);
-};
-
-
-class FullModelChecker : public QModelBuilder
-{
-protected:
- Node d_true;
- Node d_false;
- std::map<TypeNode, std::map< Node, int > > d_rep_ids;
- std::map<Node, Def > d_quant_models;
- std::map<Node, Node > d_quant_cond;
- std::map< TypeNode, Node > d_array_cond;
- std::map< Node, Node > d_array_term_cond;
- std::map<Node, std::map< Node, int > > d_quant_var_id;
- std::map<Node, std::vector< int > > d_star_insts;
- void initializeType( FirstOrderModelFmc * fm, TypeNode tn );
- Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
- bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
-protected:
- void makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
- std::map< int, std::map< int, Node > >& changed_vals );
- void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
- std::map< int, std::map< int, Node > >& changed_vals );
-private:
- void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
-
- void doNegate( Def & dc );
- void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq );
- void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);
- void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
-
- void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,
- Def & df, std::vector< Def > & dc, int index,
- std::vector< Node > & cond, std::vector<Node> & val );
- void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
- std::map< int, Node > & entries, int index,
- std::vector< Node > & cond, std::vector< Node > & val,
- EntryTrie & curr);
-
- void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
- std::vector< Def > & dc, int index,
- std::vector< Node > & cond, std::vector<Node> & val );
- int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
- Node doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk = true );
- bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
- Node mkCond( std::vector< Node > & cond );
- Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
- void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );
- void mkCondVec( Node n, std::vector< Node > & cond );
- Node mkArrayCond( Node a );
- Node evaluateInterpreted( Node n, std::vector< Node > & vals );
- Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
-public:
- FullModelChecker( context::Context* c, QuantifiersEngine* qe );
- ~FullModelChecker(){}
-
- bool optBuildAtFullModel();
-
- int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
-
- void debugPrintCond(const char * tr, Node n, bool dispStar = false);
- void debugPrint(const char * tr, Node n, bool dispStar = false);
-
- bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
-
- Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
-
- /** process build model */
- void processBuildModel(TheoryModel* m, bool fullModel);
- /** get current model value */
- Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
-
- bool useSimpleModels();
-};
-
-}
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file full_model_check.h + ** \verbatim + ** Original author: Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Full model check class + **/ + +#ifndef FULL_MODEL_CHECK +#define FULL_MODEL_CHECK + +#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { +namespace fmcheck { + + +class FirstOrderModelFmc; +class FullModelChecker; + +class EntryTrie +{ +private: + int d_complete; +public: + EntryTrie() : d_complete(-1), d_data(-1){} + std::map<Node,EntryTrie> d_child; + int d_data; + void reset() { d_data = -1; d_child.clear(); d_complete = -1; } + void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 ); + bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 ); + int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 ); + void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true ); + + void collectIndices(Node c, int index, std::vector< int >& indices ); + bool isComplete(FirstOrderModelFmc * m, Node c, int index); +}; + + +class Def +{ +public: + EntryTrie d_et; + //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative + std::vector< Node > d_cond; + //value is returned by FullModelChecker::getRepresentative + std::vector< Node > d_value; + void basic_simplify( FirstOrderModelFmc * m ); +private: + enum { + status_unk, + status_redundant, + status_non_redundant + }; + std::vector< int > d_status; + bool d_has_simplified; +public: + Def() : d_has_simplified(false){} + void reset() { + d_et.reset(); + d_cond.clear(); + d_value.clear(); + d_status.clear(); + d_has_simplified = false; + } + bool addEntry( FirstOrderModelFmc * m, Node c, Node v); + Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ); + int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ); + void simplify( FullModelChecker * mc, FirstOrderModelFmc * m ); + void debugPrint(const char * tr, Node op, FullModelChecker * m); +}; + + +class FullModelChecker : public QModelBuilder +{ +protected: + Node d_true; + Node d_false; + std::map<TypeNode, std::map< Node, int > > d_rep_ids; + std::map<Node, Def > d_quant_models; + std::map<Node, Node > d_quant_cond; + std::map< TypeNode, Node > d_array_cond; + std::map< Node, Node > d_array_term_cond; + std::map<Node, std::map< Node, int > > d_quant_var_id; + std::map<Node, std::vector< int > > d_star_insts; + void initializeType( FirstOrderModelFmc * fm, TypeNode tn ); + Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); + bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); +protected: + void makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, + std::map< int, std::map< int, Node > >& changed_vals ); + void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, + std::map< int, std::map< int, Node > >& changed_vals ); +private: + void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ); + + void doNegate( Def & dc ); + void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ); + void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v); + void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc ); + + void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, + Def & df, std::vector< Def > & dc, int index, + std::vector< Node > & cond, std::vector<Node> & val ); + void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, + std::map< int, Node > & entries, int index, + std::vector< Node > & cond, std::vector< Node > & val, + EntryTrie & curr); + + void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, + std::vector< Def > & dc, int index, + std::vector< Node > & cond, std::vector<Node> & val ); + int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); + Node doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk = true ); + bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); + Node mkCond( std::vector< Node > & cond ); + Node mkCondDefault( FirstOrderModelFmc * fm, Node f ); + void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ); + void mkCondVec( Node n, std::vector< Node > & cond ); + Node mkArrayCond( Node a ); + Node evaluateInterpreted( Node n, std::vector< Node > & vals ); + Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); +public: + FullModelChecker( context::Context* c, QuantifiersEngine* qe ); + ~FullModelChecker(){} + + bool optBuildAtFullModel(); + + int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; } + + void debugPrintCond(const char * tr, Node n, bool dispStar = false); + void debugPrint(const char * tr, Node n, bool dispStar = false); + + bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); + + Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); + + /** process build model */ + void processBuildModel(TheoryModel* m, bool fullModel); + /** get current model value */ + Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial ); + + bool useSimpleModels(); +}; + +} +} +} +} + +#endif diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 073f7057b..5edf2de96 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -1142,4 +1142,4 @@ void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ bool QModelBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true ); -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 96d30bf37..b079ae75c 100755 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -1,182 +1,182 @@ -/********************* */
-/*! \file relevant_domain.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** 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 relevant domain class
- **/
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/relevant_domain.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-void RelevantDomain::RDomain::merge( RDomain * r ) {
- Assert( !d_parent );
- Assert( !r->d_parent );
- d_parent = r;
- for( unsigned i=0; i<d_terms.size(); i++ ){
- r->addTerm( d_terms[i] );
- }
- d_terms.clear();
-}
-
-void RelevantDomain::RDomain::addTerm( Node t ) {
- if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
- d_terms.push_back( t );
- }
-}
-
-RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
- if( !d_parent ){
- return this;
- }else{
- RDomain * p = d_parent->getParent();
- d_parent = p;
- return p;
- }
-}
-
-void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) {
- std::map< Node, Node > rterms;
- for( unsigned i=0; i<d_terms.size(); i++ ){
- Node r = d_terms[i];
- if( !TermDb::hasInstConstAttr( d_terms[i] ) ){
- r = fm->getRepresentative( d_terms[i] );
- }
- if( rterms.find( r )==rterms.end() ){
- rterms[r] = d_terms[i];
- }
- }
- d_terms.clear();
- for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){
- d_terms.push_back( it->second );
- }
-}
-
-
-
-RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){
-
-}
-
-RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) {
- if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
- d_rel_doms[n][i] = new RDomain;
- d_rn_map[d_rel_doms[n][i]] = n;
- d_ri_map[d_rel_doms[n][i]] = i;
- }
- return d_rel_doms[n][i]->getParent();
-}
-
-void RelevantDomain::compute(){
- for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
- for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- it2->second->reset();
- }
- }
- for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
- Node f = d_model->getAssertedQuantifier( i );
- Node icf = d_qe->getTermDatabase()->getInstConstantBody( f );
- Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
- computeRelevantDomain( icf, true, true );
- }
-
- Trace("rel-dom-debug") << "account for ground terms" << std::endl;
- for( std::map< Node, std::vector< Node > >::iterator it = d_model->d_uf_terms.begin(); it != d_model->d_uf_terms.end(); ++it ){
- Node op = it->first;
- for( unsigned i=0; i<it->second.size(); i++ ){
- Node n = it->second[i];
- //if it is a non-redundant term
- if( !n.getAttribute(NoMatchAttribute()) ){
- for( unsigned j=0; j<n.getNumChildren(); j++ ){
- RDomain * rf = getRDomain( op, j );
- rf->addTerm( n[j] );
- }
- }
- }
- }
- //print debug
- for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
- Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl;
- for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- Trace("rel-dom") << " " << it2->first << " : ";
- RDomain * r = it2->second;
- RDomain * rp = r->getParent();
- if( r==rp ){
- r->removeRedundantTerms( d_model );
- for( unsigned i=0; i<r->d_terms.size(); i++ ){
- Trace("rel-dom") << r->d_terms[i] << " ";
- }
- }else{
- Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) ";
- }
- Trace("rel-dom") << std::endl;
- }
- }
-
-}
-
-void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
-
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( n.getKind()==APPLY_UF ){
- RDomain * rf = getRDomain( n.getOperator(), i );
- if( n[i].getKind()==INST_CONSTANT ){
- Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] );
- //merge the RDomains
- unsigned id = n[i].getAttribute(InstVarNumAttribute());
- Trace("rel-dom-debug") << n[i] << " is variable # " << id << " for " << q;
- Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl;
- RDomain * rq = getRDomain( q, id );
- if( rf!=rq ){
- rq->merge( rf );
- }
- }else{
- //term to add
- rf->addTerm( n[i] );
- }
- }
-
- //TODO
- if( n[i].getKind()!=FORALL ){
- bool newHasPol = hasPol;
- bool newPol = pol;
- computeRelevantDomain( n[i], newHasPol, newPol );
- }
- }
-}
-
-Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) {
- RDomain * rf = getRDomain( f, i );
- Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl;
- if( !d_qe->getEqualityQuery()->getEngine()->hasTerm( r ) || rf->hasTerm( r ) ){
- return r;
- }else{
- Node rr = d_model->getRepresentative( r );
- eq::EqClassIterator eqc( rr, d_qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( rf->hasTerm( en ) ){
- return en;
- }
- ++eqc;
- }
- //otherwise, may be equal to some non-ground term
-
- return r;
- }
-}
\ No newline at end of file +/********************* */ +/*! \file relevant_domain.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** 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 relevant domain class + **/ + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +void RelevantDomain::RDomain::merge( RDomain * r ) { + Assert( !d_parent ); + Assert( !r->d_parent ); + d_parent = r; + for( unsigned i=0; i<d_terms.size(); i++ ){ + r->addTerm( d_terms[i] ); + } + d_terms.clear(); +} + +void RelevantDomain::RDomain::addTerm( Node t ) { + if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){ + d_terms.push_back( t ); + } +} + +RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() { + if( !d_parent ){ + return this; + }else{ + RDomain * p = d_parent->getParent(); + d_parent = p; + return p; + } +} + +void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) { + std::map< Node, Node > rterms; + for( unsigned i=0; i<d_terms.size(); i++ ){ + Node r = d_terms[i]; + if( !TermDb::hasInstConstAttr( d_terms[i] ) ){ + r = fm->getRepresentative( d_terms[i] ); + } + if( rterms.find( r )==rterms.end() ){ + rterms[r] = d_terms[i]; + } + } + d_terms.clear(); + for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){ + d_terms.push_back( it->second ); + } +} + + + +RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){ + +} + +RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) { + if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){ + d_rel_doms[n][i] = new RDomain; + d_rn_map[d_rel_doms[n][i]] = n; + d_ri_map[d_rel_doms[n][i]] = i; + } + return d_rel_doms[n][i]->getParent(); +} + +void RelevantDomain::compute(){ + for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){ + for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + it2->second->reset(); + } + } + for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ + Node f = d_model->getAssertedQuantifier( i ); + Node icf = d_qe->getTermDatabase()->getInstConstantBody( f ); + Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl; + computeRelevantDomain( icf, true, true ); + } + + Trace("rel-dom-debug") << "account for ground terms" << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = d_model->d_uf_terms.begin(); it != d_model->d_uf_terms.end(); ++it ){ + Node op = it->first; + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + //if it is a non-redundant term + if( !n.getAttribute(NoMatchAttribute()) ){ + for( unsigned j=0; j<n.getNumChildren(); j++ ){ + RDomain * rf = getRDomain( op, j ); + rf->addTerm( n[j] ); + } + } + } + } + //print debug + for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){ + Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl; + for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + Trace("rel-dom") << " " << it2->first << " : "; + RDomain * r = it2->second; + RDomain * rp = r->getParent(); + if( r==rp ){ + r->removeRedundantTerms( d_model ); + for( unsigned i=0; i<r->d_terms.size(); i++ ){ + Trace("rel-dom") << r->d_terms[i] << " "; + } + }else{ + Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) "; + } + Trace("rel-dom") << std::endl; + } + } + +} + +void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { + + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( n.getKind()==APPLY_UF ){ + RDomain * rf = getRDomain( n.getOperator(), i ); + if( n[i].getKind()==INST_CONSTANT ){ + Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] ); + //merge the RDomains + unsigned id = n[i].getAttribute(InstVarNumAttribute()); + Trace("rel-dom-debug") << n[i] << " is variable # " << id << " for " << q; + Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl; + RDomain * rq = getRDomain( q, id ); + if( rf!=rq ){ + rq->merge( rf ); + } + }else{ + //term to add + rf->addTerm( n[i] ); + } + } + + //TODO + if( n[i].getKind()!=FORALL ){ + bool newHasPol = hasPol; + bool newPol = pol; + computeRelevantDomain( n[i], newHasPol, newPol ); + } + } +} + +Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) { + RDomain * rf = getRDomain( f, i ); + Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl; + if( !d_qe->getEqualityQuery()->getEngine()->hasTerm( r ) || rf->hasTerm( r ) ){ + return r; + }else{ + Node rr = d_model->getRepresentative( r ); + eq::EqClassIterator eqc( rr, d_qe->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + if( rf->hasTerm( en ) ){ + return en; + } + ++eqc; + } + //otherwise, may be equal to some non-ground term + + return r; + } +} diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 5939ec727..c4345f828 100755 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -1,62 +1,62 @@ -/********************* */
-/*! \file relevant_domain.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** 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 relevant domain class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class RelevantDomain
-{
-private:
- class RDomain
- {
- public:
- RDomain() : d_parent( NULL ) {}
- void reset() { d_parent = NULL; d_terms.clear(); }
- RDomain * d_parent;
- std::vector< Node > d_terms;
- void merge( RDomain * r );
- void addTerm( Node t );
- RDomain * getParent();
- void removeRedundantTerms( FirstOrderModel * fm );
- bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
- };
- std::map< Node, std::map< int, RDomain * > > d_rel_doms;
- std::map< RDomain *, Node > d_rn_map;
- std::map< RDomain *, int > d_ri_map;
- RDomain * getRDomain( Node n, int i );
- QuantifiersEngine* d_qe;
- FirstOrderModel* d_model;
- void computeRelevantDomain( Node n, bool hasPol, bool pol );
-public:
- RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
- virtual ~RelevantDomain(){}
- //compute the relevant domain
- void compute();
-
- Node getRelevantTerm( Node f, int i, Node r );
-};/* class RelevantDomain */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
+/********************* */ +/*! \file relevant_domain.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** 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 relevant domain class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H +#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H + +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class RelevantDomain +{ +private: + class RDomain + { + public: + RDomain() : d_parent( NULL ) {} + void reset() { d_parent = NULL; d_terms.clear(); } + RDomain * d_parent; + std::vector< Node > d_terms; + void merge( RDomain * r ); + void addTerm( Node t ); + RDomain * getParent(); + void removeRedundantTerms( FirstOrderModel * fm ); + bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } + }; + std::map< Node, std::map< int, RDomain * > > d_rel_doms; + std::map< RDomain *, Node > d_rn_map; + std::map< RDomain *, int > d_ri_map; + RDomain * getRDomain( Node n, int i ); + QuantifiersEngine* d_qe; + FirstOrderModel* d_model; + void computeRelevantDomain( Node n, bool hasPol, bool pol ); +public: + RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ); + virtual ~RelevantDomain(){} + //compute the relevant domain + void compute(); + + Node getRelevantTerm( Node f, int i, Node r ); +};/* class RelevantDomain */ + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index e278de9e1..107a99014 100755 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -1,184 +1,184 @@ -/********************* */
-/*! \file bounded_integers.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Rewrite engine module
- **
- ** This class manages rewrite rules for quantifiers
- **/
-
-#include "theory/quantifiers/rewrite_engine.h"
-#include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/inst_match_generator.h"
-#include "theory/theory_engine.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-struct PrioritySort {
- std::vector< double > d_priority;
- bool operator() (int i,int j) {
- return d_priority[i] < d_priority[j];
- }
-};
-
-
-RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
-
-}
-
-double RewriteEngine::getPriority( Node f ) {
- Node rr = f.getAttribute(QRewriteRuleAttribute());
- Node rrr = rr[2];
- Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;
- bool deterministic = rrr[1].getKind()!=OR;
- if( rrr.getKind()==RR_REWRITE ){
- return deterministic ? 0.0 : 3.0;
- }else if( rrr.getKind()==RR_DEDUCTION ){
- return deterministic ? 1.0 : 4.0;
- }else if( rrr.getKind()==RR_REDUCTION ){
- return deterministic ? 2.0 : 5.0;
- }else{
- return 6.0;
- }
-}
-
-void RewriteEngine::check( Theory::Effort e ) {
- if( e==Theory::EFFORT_LAST_CALL ){
- if( !d_quantEngine->getModel()->isModelSet() ){
- d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );
- }
- if( d_true.isNull() ){
- d_true = NodeManager::currentNM()->mkConst( true );
- }
- std::vector< Node > priority_order;
- PrioritySort ps;
- std::vector< int > indicies;
- for( int i=0; i<(int)d_rr_quant.size(); i++ ){
- ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );
- indicies.push_back( i );
- }
- std::sort( indicies.begin(), indicies.end(), ps );
- for( unsigned i=0; i<indicies.size(); i++ ){
- priority_order.push_back( d_rr_quant[indicies[i]] );
- }
-
- //apply rewrite rules
- int addedLemmas = 0;
- //per priority level
- int index = 0;
- bool success = true;
- while( success && index<(int)priority_order.size() ) {
- addedLemmas += checkRewriteRule( priority_order[index] );
- index++;
- if( index<(int)priority_order.size() ){
- success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] );
- }
- }
-
- Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;
- if (addedLemmas==0) {
- }else{
- //otherwise, the search will continue
- d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
- }
- }
-}
-
-int RewriteEngine::checkRewriteRule( Node f ) {
- Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl;
- int addedLemmas = 0;
- //reset triggers
- Node rr = f.getAttribute(QRewriteRuleAttribute());
- if( d_rr_triggers.find(f)==d_rr_triggers.end() ){
- std::vector< inst::Trigger * > triggers;
- if( f.getNumChildren()==3 ){
- for(unsigned i=0; i<f[2].getNumChildren(); i++ ){
- Node pat = f[2][i];
- std::vector< Node > nodes;
- Trace("rewrite-engine-trigger") << "Trigger is : ";
- for( int j=0; j<(int)pat.getNumChildren(); j++ ){
- Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f );
- nodes.push_back( p );
- Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " ";
- }
- Trace("rewrite-engine-trigger") << std::endl;
- Assert( inst::Trigger::isUsableTrigger( nodes, f ) );
- inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false );
- tr->getGenerator()->setActiveAdd(false);
- triggers.push_back( tr );
- }
- }
- d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() );
- }
- for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){
- Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl;
- d_rr_triggers[f][i]->resetInstantiationRound();
- d_rr_triggers[f][i]->reset( Node::null() );
- bool success;
- do
- {
- InstMatch m;
- success = d_rr_triggers[f][i]->getNextMatch( f, m );
- if( success ){
- //see if instantiation is true in the model
- Node rr = f.getAttribute(QRewriteRuleAttribute());
- Node rrg = rr[1];
- std::vector< Node > vars;
- std::vector< Node > terms;
- d_quantEngine->computeTermVector( f, m, vars, terms );
- Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl;
- Node inst = d_rr_guard[f];
- inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
- Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl;
- FirstOrderModel * fm = d_quantEngine->getModel();
- Node v = fm->getValue( inst );
- Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl;
- if( v==d_true ){
- Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;
- if( d_quantEngine->addInstantiation( f, m ) ){
- addedLemmas++;
- Trace("rewrite-engine-inst-debug") << "success" << std::endl;
- //set the no-match attribute (the term is rewritten and can be ignored)
- //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl;
- //if( !m.d_matched.isNull() ){
- // NoMatchAttribute nma;
- // m.d_matched.setAttribute(nma,true);
- //}
- }else{
- Trace("rewrite-engine-inst-debug") << "failure." << std::endl;
- }
- }
- }
- }while(success);
- }
- Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl;
- return addedLemmas;
-}
-
-void RewriteEngine::registerQuantifier( Node f ) {
- if( f.hasAttribute(QRewriteRuleAttribute()) ){
- Trace("rewrite-engine") << "Register quantifier " << f << std::endl;
- Node rr = f.getAttribute(QRewriteRuleAttribute());
- Trace("rewrite-engine") << " rewrite rule is : " << rr << std::endl;
- d_rr_quant.push_back( f );
- d_rr_guard[f] = rr[1];
- Trace("rewrite-engine") << " guard is : " << d_rr_guard[f] << std::endl;
- }
-}
-
-void RewriteEngine::assertNode( Node n ) {
-
-}
-
+/********************* */ +/*! \file bounded_integers.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Rewrite engine module + ** + ** This class manages rewrite rules for quantifiers + **/ + +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/inst_match_generator.h" +#include "theory/theory_engine.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +struct PrioritySort { + std::vector< double > d_priority; + bool operator() (int i,int j) { + return d_priority[i] < d_priority[j]; + } +}; + + +RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { + +} + +double RewriteEngine::getPriority( Node f ) { + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Node rrr = rr[2]; + Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl; + bool deterministic = rrr[1].getKind()!=OR; + if( rrr.getKind()==RR_REWRITE ){ + return deterministic ? 0.0 : 3.0; + }else if( rrr.getKind()==RR_DEDUCTION ){ + return deterministic ? 1.0 : 4.0; + }else if( rrr.getKind()==RR_REDUCTION ){ + return deterministic ? 2.0 : 5.0; + }else{ + return 6.0; + } +} + +void RewriteEngine::check( Theory::Effort e ) { + if( e==Theory::EFFORT_LAST_CALL ){ + if( !d_quantEngine->getModel()->isModelSet() ){ + d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true ); + } + if( d_true.isNull() ){ + d_true = NodeManager::currentNM()->mkConst( true ); + } + std::vector< Node > priority_order; + PrioritySort ps; + std::vector< int > indicies; + for( int i=0; i<(int)d_rr_quant.size(); i++ ){ + ps.d_priority.push_back( getPriority( d_rr_quant[i] ) ); + indicies.push_back( i ); + } + std::sort( indicies.begin(), indicies.end(), ps ); + for( unsigned i=0; i<indicies.size(); i++ ){ + priority_order.push_back( d_rr_quant[indicies[i]] ); + } + + //apply rewrite rules + int addedLemmas = 0; + //per priority level + int index = 0; + bool success = true; + while( success && index<(int)priority_order.size() ) { + addedLemmas += checkRewriteRule( priority_order[index] ); + index++; + if( index<(int)priority_order.size() ){ + success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] ); + } + } + + Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl; + if (addedLemmas==0) { + }else{ + //otherwise, the search will continue + d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); + } + } +} + +int RewriteEngine::checkRewriteRule( Node f ) { + Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl; + int addedLemmas = 0; + //reset triggers + Node rr = f.getAttribute(QRewriteRuleAttribute()); + if( d_rr_triggers.find(f)==d_rr_triggers.end() ){ + std::vector< inst::Trigger * > triggers; + if( f.getNumChildren()==3 ){ + for(unsigned i=0; i<f[2].getNumChildren(); i++ ){ + Node pat = f[2][i]; + std::vector< Node > nodes; + Trace("rewrite-engine-trigger") << "Trigger is : "; + for( int j=0; j<(int)pat.getNumChildren(); j++ ){ + Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f ); + nodes.push_back( p ); + Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " "; + } + Trace("rewrite-engine-trigger") << std::endl; + Assert( inst::Trigger::isUsableTrigger( nodes, f ) ); + inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false ); + tr->getGenerator()->setActiveAdd(false); + triggers.push_back( tr ); + } + } + d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() ); + } + for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){ + Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl; + d_rr_triggers[f][i]->resetInstantiationRound(); + d_rr_triggers[f][i]->reset( Node::null() ); + bool success; + do + { + InstMatch m; + success = d_rr_triggers[f][i]->getNextMatch( f, m ); + if( success ){ + //see if instantiation is true in the model + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Node rrg = rr[1]; + std::vector< Node > vars; + std::vector< Node > terms; + d_quantEngine->computeTermVector( f, m, vars, terms ); + Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl; + Node inst = d_rr_guard[f]; + inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl; + FirstOrderModel * fm = d_quantEngine->getModel(); + Node v = fm->getValue( inst ); + Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl; + if( v==d_true ){ + Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl; + if( d_quantEngine->addInstantiation( f, m ) ){ + addedLemmas++; + Trace("rewrite-engine-inst-debug") << "success" << std::endl; + //set the no-match attribute (the term is rewritten and can be ignored) + //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl; + //if( !m.d_matched.isNull() ){ + // NoMatchAttribute nma; + // m.d_matched.setAttribute(nma,true); + //} + }else{ + Trace("rewrite-engine-inst-debug") << "failure." << std::endl; + } + } + } + }while(success); + } + Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl; + return addedLemmas; +} + +void RewriteEngine::registerQuantifier( Node f ) { + if( f.hasAttribute(QRewriteRuleAttribute()) ){ + Trace("rewrite-engine") << "Register quantifier " << f << std::endl; + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Trace("rewrite-engine") << " rewrite rule is : " << rr << std::endl; + d_rr_quant.push_back( f ); + d_rr_guard[f] = rr[1]; + Trace("rewrite-engine") << " guard is : " << d_rr_guard[f] << std::endl; + } +} + +void RewriteEngine::assertNode( Node n ) { + +} + diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 6783b20d0..2d9d751c2 100755 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -1,54 +1,54 @@ -/********************* */
-/*! \file bounded_integers.h
-** \verbatim
-** Original author: Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013 New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief This class manages integer bounds for quantifiers
-**/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__REWRITE_ENGINE_H
-#define __CVC4__REWRITE_ENGINE_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "context/cdchunk_list.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class RewriteEngine : public QuantifiersModule
-{
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
- std::vector< Node > d_rr_quant;
- std::map< Node, Node > d_rr_guard;
- Node d_true;
- /** explicitly provided patterns */
- std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
- double getPriority( Node f );
-private:
- int checkRewriteRule( Node f );
-public:
- RewriteEngine( context::Context* c, QuantifiersEngine* qe );
-
- void check( Theory::Effort e );
- void registerQuantifier( Node f );
- void assertNode( Node n );
-};
-
-}
-}
-}
-
-#endif
\ No newline at end of file +/********************* */ +/*! \file bounded_integers.h +** \verbatim +** Original author: Andrew Reynolds +** This file is part of the CVC4 project. +** Copyright (c) 2009-2013 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief This class manages integer bounds for quantifiers +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__REWRITE_ENGINE_H +#define __CVC4__REWRITE_ENGINE_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/trigger.h" + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdchunk_list.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class RewriteEngine : public QuantifiersModule +{ + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + std::vector< Node > d_rr_quant; + std::map< Node, Node > d_rr_guard; + Node d_true; + /** explicitly provided patterns */ + std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; + double getPriority( Node f ); +private: + int checkRewriteRule( Node f ); +public: + RewriteEngine( context::Context* c, QuantifiersEngine* qe ); + + void check( Theory::Effort e ); + void registerQuantifier( Node f ); + void assertNode( Node n ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f94a87748..e5cc8a1fb 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -750,4 +750,4 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){ bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() { return false; //shown to be not effective -}
\ No newline at end of file +} diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h index 256957855..fa6bb2227 100644 --- a/src/theory/rewriterules/theory_rewriterules_type_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h @@ -33,6 +33,8 @@ public: * Compute the type for (and optionally typecheck) a term belonging * to the theory of rewriterules. * + * @param nodeManager the NodeManager in use + * @param n the node to compute the type of * @param check if true, the node's type should be checked as well * as computed. */ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index c8b7d76eb..adcf78a86 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1857,4 +1857,4 @@ DisequalityPropagator::Statistics::Statistics(): DisequalityPropagator::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(& d_propagations); -}
\ No newline at end of file +} diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 1e27fa859..da2af6c1f 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -155,10 +155,10 @@ public: #ifdef CVC4_NEED_INT64_T_OVERLOADS Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) { - d_value /= static_cast<long>(d); + d_value /= cln::cl_I(d); } Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) { - d_value /= static_cast<unsigned long>(d); + d_value /= cln::cl_I(d); } #endif /* CVC4_NEED_INT64_T_OVERLOADS */ diff --git a/test/system/Makefile.am b/test/system/Makefile.am index d79fcb7ba..c279a3d26 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -89,9 +89,9 @@ $(filter-out %.class.lo,$(TESTS:%=%.lo)): %.lo: %.cpp $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $+ $(filter-out %.class,$(TESTS)): %: %.lo $(LIBADD) $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $(LIBS) $< -#cvc3_main: cvc3_george.lo $(LIBADD) -cvc3_main: $(LIBADD) - $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $(LIBS) $+ +cvc3_main: cvc3_george.lo $(LIBADD) +#cvc3_main: $(LIBADD) +# $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $(LIBS) $+ CVC4JavaTest.class: CVC4JavaTest.java @abs_top_builddir@/src/bindings/CVC4.jar @abs_top_builddir@/src/bindings/java/libcvc4jni.la $(AM_V_JAVAC)$(JAVAC) -classpath @abs_top_builddir@/src/bindings/CVC4.jar -d $(builddir) $< |