diff options
author | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
---|---|---|
committer | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
commit | 36a0d1d948f201471596e092136c5a00103f78af (patch) | |
tree | 7a9b0d79074da1cb0c1cbed986584d50792a30e9 /src/theory/quantifiers/ceg_instantiator.cpp | |
parent | 66525e81928d0d025dbcc197ab3ef772eac31103 (diff) | |
parent | a58abbe71fb1fc07129ff9c7568ac544145fb57c (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4.git
Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.cpp')
-rwxr-xr-x[-rw-r--r--] | src/theory/quantifiers/ceg_instantiator.cpp | 48 |
1 files changed, 46 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index da488ea98..cd263e90c 100644..100755 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -22,6 +22,9 @@ #include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" + //#define MBP_STRICT_ASSERTIONS using namespace std; @@ -466,6 +469,36 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: } } } + /* TODO: algebraic reasoning for bitvector instantiation + else if( pvtn.isBitVector() ){ + if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){ + for( unsigned t=0; t<2; t++ ){ + if( atom[t]==pv ){ + computeProgVars( atom[1-t] ); + if( d_inelig.find( atom[1-t] )==d_inelig.end() ){ + //only ground terms TODO: more + if( d_prog_var[atom[1-t]].empty() ){ + Node veq_c; + Node uval; + if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){ + uval = atom[1-t]; + }else{ + uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], + bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) ); + } + if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ + subs_proc[uval][veq_c] = true; + if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; + } + } + } + } + } + } + } + } + */ } } } @@ -685,7 +718,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: //[5] resort to using value in model // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype - if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ + if( ( effort>0 || pvtn.isBoolean() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ Node mv = getModelValue( pv ); Node pv_coeff_m; Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl; @@ -781,6 +814,7 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int } } if( success ){ + Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl; vars.push_back( pv ); btyp.push_back( bt ); sf.push_back( pv, n, pv_coeff ); @@ -800,8 +834,10 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int curr_var.pop_back(); is_cv = true; } + Trace("cbqi-inst-debug2") << "Recurse..." << std::endl; success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); if( !success ){ + Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; if( is_cv ){ curr_var.push_back( pv ); } @@ -814,6 +850,7 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int if( success ){ return true; }else{ + Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl; //revert substitution information for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ sf.d_subs[it->first] = it->second; @@ -1035,7 +1072,13 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node if( !it->second.isNull() ){ c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); } - Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); + Assert( !c_coeff.isNull() ); + Node c; + if( msum_term[it->first].isNull() ){ + c = c_coeff; + }else{ + c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); + } children.push_back( c ); Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl; } @@ -1594,6 +1637,7 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); Assert( d_out->isEligibleForInstantiation( realPart ) ); //re-isolate + Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl; ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; |