From da9eec6aa0fc0f6c29f2c3fdb08bd45ba9c27808 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 29 Jul 2013 16:08:45 -0400 Subject: [PATCH] Fix numerous compiler warnings on various platforms --- config/cvc4.m4 | 16 + config/doxygen.cfg | 2 +- configure.ac | 7 +- src/bindings/Makefile.am | 6 +- src/expr/metakind_template.h | 12 +- src/options/options_template.cpp | 4 +- src/parser/cvc/Makefile.am | 2 +- src/theory/arith/error_set.cpp | 12 +- src/theory/arith/error_set.h | 10 +- src/theory/bv/bitblaster.cpp | 4 +- src/theory/bv/bitblaster.h | 3 +- src/theory/idl/options | 2 + src/theory/quantifiers/bounded_integers.cpp | 732 ++--- src/theory/quantifiers/bounded_integers.h | 252 +- .../quantifiers/candidate_generator.cpp | 2 +- .../quantifiers/first_order_reasoning.cpp | 342 +- .../quantifiers/first_order_reasoning.h | 90 +- src/theory/quantifiers/full_model_check.cpp | 2796 ++++++++--------- src/theory/quantifiers/full_model_check.h | 316 +- src/theory/quantifiers/model_builder.cpp | 2 +- src/theory/quantifiers/relevant_domain.cpp | 364 +-- src/theory/quantifiers/relevant_domain.h | 124 +- src/theory/quantifiers/rewrite_engine.cpp | 368 +-- src/theory/quantifiers/rewrite_engine.h | 108 +- src/theory/quantifiers_engine.cpp | 2 +- .../theory_rewriterules_type_rules.h | 2 + src/theory/uf/theory_uf_strong_solver.cpp | 2 +- src/util/rational_cln_imp.h | 4 +- test/system/Makefile.am | 6 +- 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 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& 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]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 || ifirst; - 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 >& 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; iassertNode( 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 > 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; imkNode( 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; imkSkolem( "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; iassertNode( 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; igetNextDecisionRequest(); - 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; id_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]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 || ifirst; + 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 >& 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; iassertNode( 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 > 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; imkNode( 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; imkSkolem( "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; iassertNode( 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; igetNextDecisionRequest(); + 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; id_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 NodeBoolMap; - typedef context::CDHashMap NodeIntMap; - typedef context::CDHashMap 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 NodeBoolMap; + typedef context::CDHashMap NodeIntMap; + typedef context::CDHashMap 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 - -#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 & lits ){ - if( n.getKind()==FORALL ){ - collectLits( n[1], lits ); - }else if( n.getKind()==OR ){ - for(unsigned j=0; j& assertions ){ - for( unsigned i=0; i 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; jmkConst(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 & lits) { - int index = -1; - for( unsigned i=0; imkConst( 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; imkNode( 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 + +#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 & lits ){ + if( n.getKind()==FORALL ){ + collectLits( n[1], lits ); + }else if( n.getKind()==OR ){ + for(unsigned j=0; j& assertions ){ + for( unsigned i=0; i 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; jmkConst(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 & lits) { + int index = -1; + for( unsigned i=0; imkConst( 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; imkNode( 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 -#include -#include -#include -#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 & 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 +#include +#include +#include +#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 & 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() < d_terms[j].getConst() ); - } -}; - - -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::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 & 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::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 && gindexgetStar(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 & compat, std::vector & 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::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::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 compat; - std::vector gen; - d_et.getEntries(m, c, compat, gen); - for( unsigned i=0; i& 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& 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; iisInterval(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; idebugPrintCond(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; asecond.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; isecond.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::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::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; id_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; id_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 children; - std::vector< Node > entry_children; - children.push_back(op); - entry_children.push_back(op); - bool hasNonStar = false; - for( unsigned i=0; igetUsedRepresentative( 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; id_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; jd_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; id_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::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; j0 ) 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; imkFunctionType( 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 inst; - for (unsigned j=0; jisStar(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; jaddInstantiation( 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; iisInterval(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; iisInterval(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; igetUsedRepresentative( 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; iaddInstantiation( 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(); - 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 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; id_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; iisStar(dc.d_cond[i][j])) { - std::vector 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 & val ) { - Trace("fmc-uf-process") << "process at " << index << std::endl; - for( unsigned i=1; i 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 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 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::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::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::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 & 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 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; iisStar(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; iisStar(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() < b2.getConst() ){ - 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() < b[1].getConst() ){ - 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; igetStarElement( 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; imkFunctionType( 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 children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - for (unsigned i=0; imkNode(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; id_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; id_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; id_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; igetStar( 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 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() < d_terms[j].getConst() ); + } +}; + + +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::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 & 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::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 && gindexgetStar(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 & compat, std::vector & 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::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::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 compat; + std::vector gen; + d_et.getEntries(m, c, compat, gen); + for( unsigned i=0; i& 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& 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; iisInterval(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; idebugPrintCond(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; asecond.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; isecond.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::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::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; id_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; id_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 children; + std::vector< Node > entry_children; + children.push_back(op); + entry_children.push_back(op); + bool hasNonStar = false; + for( unsigned i=0; igetUsedRepresentative( 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; id_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; jd_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; id_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::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; j0 ) 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; imkFunctionType( 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 inst; + for (unsigned j=0; jisStar(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; jaddInstantiation( 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; iisInterval(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; iisInterval(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; igetUsedRepresentative( 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; iaddInstantiation( 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(); + 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 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; id_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; iisStar(dc.d_cond[i][j])) { + std::vector 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 & val ) { + Trace("fmc-uf-process") << "process at " << index << std::endl; + for( unsigned i=1; i 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 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 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::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::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::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 & 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 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; iisStar(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; iisStar(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() < b2.getConst() ){ + 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() < b[1].getConst() ){ + 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; igetStarElement( 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; imkFunctionType( 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 children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for (unsigned i=0; imkNode(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; id_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; id_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; id_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; igetStar( 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 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 & inst, int index = 0 ); - void getEntries( FirstOrderModelFmc * m, Node c, std::vector & compat, std::vector & 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& inst ); - int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector& 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 > d_rep_ids; - std::map d_quant_models; - std::map d_quant_cond; - std::map< TypeNode, Node > d_array_cond; - std::map< Node, Node > d_array_term_cond; - std::map > d_quant_var_id; - std::map > 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 & 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 & 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 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 & inst, int index = 0 ); + void getEntries( FirstOrderModelFmc * m, Node c, std::vector & compat, std::vector & 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& inst ); + int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector& 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 > d_rep_ids; + std::map d_quant_models; + std::map d_quant_cond; + std::map< TypeNode, Node > d_array_cond; + std::map< Node, Node > d_array_term_cond; + std::map > d_quant_var_id; + std::map > 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 & 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 & 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; iaddTerm( 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; igetRepresentative( 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; isecond.size(); i++ ){ - Node n = it->second[i]; - //if it is a non-redundant term - if( !n.getAttribute(NoMatchAttribute()) ){ - for( unsigned j=0; jaddTerm( 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; id_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; igetTermDatabase()->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; iaddTerm( 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; igetRepresentative( 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; isecond.size(); i++ ){ + Node n = it->second[i]; + //if it is a non-redundant term + if( !n.getAttribute(NoMatchAttribute()) ){ + for( unsigned j=0; jaddTerm( 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; id_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; igetTermDatabase()->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; iflushLemmas( &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 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; iresetInstantiationRound(); - 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; iflushLemmas( &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 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; iresetInstantiationRound(); + 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 NodeBoolMap; - typedef context::CDHashMap NodeIntMap; - typedef context::CDHashMap 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 NodeBoolMap; + typedef context::CDHashMap NodeIntMap; + typedef context::CDHashMap 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(n)) { - d_value /= static_cast(d); + d_value /= cln::cl_I(d); } Rational(uint64_t n, uint64_t d) : d_value(static_cast(n)) { - d_value /= static_cast(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) $< -- 2.30.2