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

1 files changed, 22 insertions, 7 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 74b3011a6..4d228bbad 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -54,6 +54,8 @@ option purifyQuant --purify-quant bool :default false
  purify quantified formulas
 option elimExtArithQuant --elim-ext-arith-quant bool :default true
  eliminate extended arithmetic symbols in quantified formulas
+option condRewriteQuant --cond-rewrite-quant bool :default true
+ conditional rewriting of quantified formulas
  
 #### E-matching options
  
@@ -109,6 +111,8 @@ option instLevelInputOnly --inst-level-input-only bool :default true
  only input terms are assigned instantiation level zero
 option quantRepMode --quant-rep-mode=MODE  CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode
  selection mode for representatives in quantifiers engine
+option instRelevantCond --inst-rlv-cond bool :default false
+ add relevancy conditions for instantiations
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
@@ -120,7 +124,7 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
 option fullSaturateInst --fs-inst bool :default false
  interleave full saturate instantiation with other techniques
 
-option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_USE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
  choose literal matching mode
 
 ### finite model finding options
@@ -144,7 +148,7 @@ option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default fa
 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
  only add instantiations for one quantifier per round for mbqi
 
-option fmfInstEngine --fmf-inst-engine bool :default false
+option fmfInstEngine --fmf-inst-engine bool :default false :read-write
  use instantiation engine in conjunction with finite model finding
 option fmfInstGen --fmf-inst-gen bool :default true
  enable Inst-Gen instantiation techniques for finite model finding 
@@ -171,13 +175,23 @@ option qcfTConstraint --qcf-tconstraint bool :read-write :default false
  enable entailment checks for t-constraints in qcf algorithm
 option qcfAllConflict --qcf-all-conflict bool :read-write :default false
  add all available conflicting instances during conflict-based instantiation
+option qcfNestedConflict --qcf-nested-conflict bool :default false
+ consider conflicts for nested quantifiers
+option qcfVoExp --qcf-vo-exp bool :default false
+ qcf experimental variable ordering
+ 
+ 
 
 option instNoEntail --inst-no-entail bool :read-write :default true
  do not consider instances of quantified formulas that are currently entailed
 
-option instPropagate --inst-propagate bool :read-write :default false
+option instPropagate --inst-prop bool :read-write :default false
  internal propagation for instantiations for selecting relevant instances
  
+option qcfEagerTest --qcf-eager-test bool :default true
+ optimization, test qcf instances eagerly
+option qcfSkipRd --qcf-skip-rd bool :default false
+ optimization, skip instances based on possibly irrelevant portions of quantified formulas
 ### rewrite rules options 
  
 option quantRewriteRules --rewrite-rules bool :default false
@@ -219,8 +233,8 @@ option ceGuidedInst --cegqi bool :default false :read-write
   counterexample-guided quantifier instantiation
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler stringToCegqiFairMode
   if and how to apply fairness for cegqi
-option cegqiSingleInv --cegqi-si bool :default false :read-write
-  process single invocation synthesis conjectures
+option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write
+  mode for processing single invocation synthesis conjectures
 option cegqiSingleInvPartial --cegqi-si-partial bool :default false
   combined techniques for synthesis conjectures that are partially single invocation 
 option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
@@ -229,8 +243,6 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if synthesis conjecture is not single invocation
-option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
-  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
@@ -248,6 +260,9 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
 option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
   template mode for sygus invariant synthesis
 
+option sygusDirectEval --sygus-direct-eval bool :default true
+  direct unfolding of evaluation functions
+  
 # approach applied to general quantified formulas
 option cbqiSplx --cbqi-splx bool :read-write :default false
  turns on old implementation of counterexample-based quantifier instantiation