diff options
Diffstat (limited to 'src/options')
52 files changed, 318 insertions, 186 deletions
diff --git a/src/options/argument_extender.h b/src/options/argument_extender.h index 9e52691ed..e3cec3c25 100644 --- a/src/options/argument_extender.h +++ b/src/options/argument_extender.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Paul Meng, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_H -#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_H +#ifndef CVC4__OPTIONS__ARGUMENT_EXTENDER_H +#define CVC4__OPTIONS__ARGUMENT_EXTENDER_H #include <cstddef> @@ -82,4 +82,4 @@ public: }/* CVC4::options namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_H */ +#endif /* CVC4__OPTIONS__ARGUMENT_EXTENDER_H */ diff --git a/src/options/argument_extender_implementation.cpp b/src/options/argument_extender_implementation.cpp index 7c8549627..0d789c626 100644 --- a/src/options/argument_extender_implementation.cpp +++ b/src/options/argument_extender_implementation.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/argument_extender_implementation.h b/src/options/argument_extender_implementation.h index 66b21ce8c..9906bb420 100644 --- a/src/options/argument_extender_implementation.h +++ b/src/options/argument_extender_implementation.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Paul Meng, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H -#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H +#ifndef CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H +#define CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H #include <cstddef> #include <list> @@ -112,4 +112,4 @@ class ArgumentExtenderImplementation : public ArgumentExtender { }/* CVC4::options namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H */ +#endif /* CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H */ diff --git a/src/options/arith_heuristic_pivot_rule.cpp b/src/options/arith_heuristic_pivot_rule.cpp index 00ac7ab5d..6c1312dbf 100644 --- a/src/options/arith_heuristic_pivot_rule.cpp +++ b/src/options/arith_heuristic_pivot_rule.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/arith_heuristic_pivot_rule.h b/src/options/arith_heuristic_pivot_rule.h index f79a796b9..2caa21043 100644 --- a/src/options/arith_heuristic_pivot_rule.h +++ b/src/options/arith_heuristic_pivot_rule.h @@ -2,9 +2,9 @@ /*! \file arith_heuristic_pivot_rule.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H -#define __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H +#ifndef CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H +#define CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H #include <iostream> @@ -35,4 +35,4 @@ std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) CVC4_PUBLIC }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */ +#endif /* CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */ diff --git a/src/options/arith_propagation_mode.cpp b/src/options/arith_propagation_mode.cpp index 09a78b92a..895a01381 100644 --- a/src/options/arith_propagation_mode.cpp +++ b/src/options/arith_propagation_mode.cpp @@ -2,9 +2,9 @@ /*! \file arith_propagation_mode.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/arith_propagation_mode.h b/src/options/arith_propagation_mode.h index 0d54d901b..b2c6b4c61 100644 --- a/src/options/arith_propagation_mode.h +++ b/src/options/arith_propagation_mode.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H -#define __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H +#ifndef CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H +#define CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H #include <iostream> @@ -35,4 +35,4 @@ std::ostream& operator<<(std::ostream& out, ArithPropagationMode rule) CVC4_PUBL }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */ +#endif /* CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */ diff --git a/src/options/arith_unate_lemma_mode.cpp b/src/options/arith_unate_lemma_mode.cpp index a1f8d5613..34fbeb3b2 100644 --- a/src/options/arith_unate_lemma_mode.cpp +++ b/src/options/arith_unate_lemma_mode.cpp @@ -2,9 +2,9 @@ /*! \file arith_unate_lemma_mode.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/arith_unate_lemma_mode.h b/src/options/arith_unate_lemma_mode.h index 4cec65011..a917b83fd 100644 --- a/src/options/arith_unate_lemma_mode.h +++ b/src/options/arith_unate_lemma_mode.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H -#define __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H +#ifndef CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H +#define CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H #include <iostream> @@ -35,4 +35,4 @@ std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode rule) CVC4_PUBLI }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */ +#endif /* CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */ diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h index 0f1d735d1..fae6549f3 100644 --- a/src/options/base_handlers.h +++ b/src/options/base_handlers.h @@ -2,9 +2,9 @@ /*! \file base_handlers.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__BASE_HANDLERS_H -#define __CVC4__BASE_HANDLERS_H +#ifndef CVC4__BASE_HANDLERS_H +#define CVC4__BASE_HANDLERS_H #include <iostream> #include <string> @@ -83,4 +83,4 @@ struct not_equal : public comparator<std::not_equal_to> { }/* CVC4::options namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__BASE_HANDLERS_H */ +#endif /* CVC4__BASE_HANDLERS_H */ diff --git a/src/options/bool_to_bv_mode.cpp b/src/options/bool_to_bv_mode.cpp index 670e15419..12fd3c1f9 100644 --- a/src/options/bool_to_bv_mode.cpp +++ b/src/options/bool_to_bv_mode.cpp @@ -1,18 +1,18 @@ /********************* */ /*! \file bool_to_bv_mode.cpp -** \verbatim -** Top contributors (to current version): -** Makai Mann -** This file is part of the CVC4 project. -** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS -** in the top-level source directory) and their institutional affiliations. -** All rights reserved. See the file COPYING in the top-level source -** directory for licensing information.\endverbatim -** -** \brief Modes for bool-to-bv preprocessing pass -** -** Modes for bool-to-bv preprocessing pass which tries to lower booleans -** to bit-vectors of width 1 at various levels of aggressiveness. + ** \verbatim + ** Top contributors (to current version): + ** Makai Mann + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + + ** \todo document this file + **/ #include "options/bool_to_bv_mode.h" diff --git a/src/options/bool_to_bv_mode.h b/src/options/bool_to_bv_mode.h index f2911c339..2dbd723c9 100644 --- a/src/options/bool_to_bv_mode.h +++ b/src/options/bool_to_bv_mode.h @@ -1,24 +1,24 @@ /********************* */ /*! \file bool_to_bv_mode.h -** \verbatim -** Top contributors (to current version): -** Makai Mann -** This file is part of the CVC4 project. -** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS -** in the top-level source directory) and their institutional affiliations. -** All rights reserved. See the file COPYING in the top-level source -** directory for licensing information.\endverbatim -** -** \brief Modes for bool-to-bv preprocessing pass -** -** Modes for bool-to-bv preprocessing pass which tries to lower booleans -** to bit-vectors of width 1 at various levels of aggressiveness. + ** \verbatim + ** Top contributors (to current version): + ** Makai Mann + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + + ** \todo document this file + **/ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H -#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H +#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H +#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H #include <iosfwd> @@ -54,4 +54,4 @@ std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode } -#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */ diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp index 59a97c5a2..d2425831a 100644 --- a/src/options/bv_bitblast_mode.cpp +++ b/src/options/bv_bitblast_mode.cpp @@ -2,9 +2,9 @@ /*! \file bv_bitblast_mode.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King + ** Liana Hadarean, Alex Ozdemir ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -81,4 +81,25 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format) return out; } +std::ostream& operator<<(std::ostream& out, + theory::bv::BvOptimizeSatProof level) +{ + switch (level) + { + case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE: + out << "BITVECTOR_OPTIMIZE_SAT_PROOF_NONE"; + break; + case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF: + out << "BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF"; + break; + case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA: + out << "BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA"; + break; + default: out << "BvOptimizeSatProof:UNKNOWN![" << unsigned(level) << "]"; + } + + return out; +} + }/* CVC4 namespace */ + diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h index fa5791ac9..7243c38e1 100644 --- a/src/options/bv_bitblast_mode.h +++ b/src/options/bv_bitblast_mode.h @@ -2,9 +2,9 @@ /*! \file bv_bitblast_mode.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Mathias Preiner + ** Liana Hadarean, Alex Ozdemir, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H -#define __CVC4__THEORY__BV__BITBLAST_MODE_H +#ifndef CVC4__THEORY__BV__BITBLAST_MODE_H +#define CVC4__THEORY__BV__BITBLAST_MODE_H #include <iosfwd> @@ -88,6 +88,27 @@ enum BvProofFormat BITVECTOR_PROOF_LRAT, }; +/** + * When the BV solver does eager bit-blasting backed by DRAT-producing SAT solvers, proofs + * can be written in a variety of formats. + */ +enum BvOptimizeSatProof +{ + /** + * Do not optimize the SAT proof. + */ + BITVECTOR_OPTIMIZE_SAT_PROOF_NONE = 0, + /** + * Optimize the SAT proof, but do not shrink the formula + */ + BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF = 1, + /** + * Optimize the SAT proof and shrink the formula + */ + BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA = 2, +}; + + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ @@ -95,7 +116,8 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode); std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode); std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode); std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format); +std::ostream& operator<<(std::ostream& out, theory::bv::BvOptimizeSatProof level); }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */ +#endif /* CVC4__THEORY__BV__BITBLAST_MODE_H */ diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index c4541f4e4..9529b7500 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -7,13 +7,24 @@ header = "options/bv_options.h" category = "expert" long = "bv-proof-format=MODE" type = "CVC4::theory::bv::BvProofFormat" - default = "CVC4::theory::bv::BITVECTOR_PROOF_LRAT" + default = "CVC4::theory::bv::BITVECTOR_PROOF_ER" handler = "stringToBvProofFormat" predicates = ["satSolverEnabledBuild"] includes = ["options/bv_bitblast_mode.h"] help = "choose which UNSAT proof format to use, see --bv-sat-solver=help" [[option]] + name = "bvOptimizeSatProof" + category = "expert" + long = "bv-optimize-sat-proof=MODE" + type = "CVC4::theory::bv::BvOptimizeSatProof" + default = "CVC4::theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA" + handler = "stringToBvOptimizeSatProof" + predicates = ["satSolverEnabledBuild"] + includes = ["options/bv_bitblast_mode.h"] + help = "enable SAT proof optimizations, see --bv-optimize-sat-proof=help" + +[[option]] name = "bvSatSolver" smt_name = "bv-sat-solver" category = "expert" diff --git a/src/options/datatypes_modes.h b/src/options/datatypes_modes.h index 5f41ce11d..8d7ced9e2 100644 --- a/src/options/datatypes_modes.h +++ b/src/options/datatypes_modes.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__BASE__DATATYPES_MODES_H -#define __CVC4__BASE__DATATYPES_MODES_H +#ifndef CVC4__BASE__DATATYPES_MODES_H +#define CVC4__BASE__DATATYPES_MODES_H #include <iostream> @@ -41,4 +41,4 @@ enum SygusFairMode { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__BASE__DATATYPES_MODES_H */ +#endif /* CVC4__BASE__DATATYPES_MODES_H */ diff --git a/src/options/decision_mode.cpp b/src/options/decision_mode.cpp index cd0bc8180..f2c37f52a 100644 --- a/src/options/decision_mode.cpp +++ b/src/options/decision_mode.cpp @@ -2,9 +2,9 @@ /*! \file decision_mode.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/decision_mode.h b/src/options/decision_mode.h index eb10ba8e8..c90e0a6f0 100644 --- a/src/options/decision_mode.h +++ b/src/options/decision_mode.h @@ -2,9 +2,9 @@ /*! \file decision_mode.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Kshitij Bansal, Tim King + ** Kshitij Bansal, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__SMT__DECISION_MODE_H -#define __CVC4__SMT__DECISION_MODE_H +#ifndef CVC4__SMT__DECISION_MODE_H +#define CVC4__SMT__DECISION_MODE_H #include <iosfwd> @@ -61,4 +61,4 @@ std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode); }/* CVC4 namespace */ -#endif /* __CVC4__SMT__DECISION_MODE_H */ +#endif /* CVC4__SMT__DECISION_MODE_H */ diff --git a/src/options/decision_weight.h b/src/options/decision_weight.h index 90f6affa5..16c12a3b4 100644 --- a/src/options/decision_weight.h +++ b/src/options/decision_weight.h @@ -2,9 +2,9 @@ /*! \file decision_weight.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Morgan Deters + ** Tim King, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__OPTIONS__DECISION_WEIGHT_H -#define __CVC4__OPTIONS__DECISION_WEIGHT_H +#ifndef CVC4__OPTIONS__DECISION_WEIGHT_H +#define CVC4__OPTIONS__DECISION_WEIGHT_H namespace CVC4 { namespace decision { @@ -27,4 +27,4 @@ typedef uint64_t DecisionWeight; }/* CVC4::decision namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__OPTIONS__DECISION_WEIGHT_H */ +#endif /* CVC4__OPTIONS__DECISION_WEIGHT_H */ diff --git a/src/options/didyoumean.cpp b/src/options/didyoumean.cpp index 3f5278b7e..cbaa4d09e 100644 --- a/src/options/didyoumean.cpp +++ b/src/options/didyoumean.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Kshitij Bansal, Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/didyoumean.h b/src/options/didyoumean.h index 4d7734771..f33716565 100644 --- a/src/options/didyoumean.h +++ b/src/options/didyoumean.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp index b01b52777..7230f544d 100644 --- a/src/options/didyoumean_test.cpp +++ b/src/options/didyoumean_test.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml index eb8c933af..af8d044f7 100644 --- a/src/options/fp_options.toml +++ b/src/options/fp_options.toml @@ -1,3 +1,11 @@ id = "FP" name = "Fp" header = "options/fp_options.h" + +[[option]] + name = "fpExp" + category = "regular" + long = "fp-exp" + type = "bool" + default = "false" + help = "Allow floating-point sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental)" diff --git a/src/options/language.cpp b/src/options/language.cpp index 089633519..4aefd742c 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/language.h b/src/options/language.h index 87a05a24f..4d213c305 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__LANGUAGE_H -#define __CVC4__LANGUAGE_H +#ifndef CVC4__LANGUAGE_H +#define CVC4__LANGUAGE_H #include <sstream> #include <string> @@ -232,4 +232,4 @@ OutputLanguage toOutputLanguage(std::string language) CVC4_PUBLIC; }/* CVC4::language namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__LANGUAGE_H */ +#endif /* CVC4__LANGUAGE_H */ diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index 636dbe89b..46162845d 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -2,9 +2,9 @@ /*! \file module_template.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner + ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/module_template.h b/src/options/module_template.h index 00bb74490..2ffe070d2 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__OPTIONS__${id}$_H -#define __CVC4__OPTIONS__${id}$_H +#ifndef CVC4__OPTIONS__${id}$_H +#define CVC4__OPTIONS__${id}$_H #include "options/options.h" @@ -48,4 +48,4 @@ ${inls}$ } // namespace options } // namespace CVC4 -#endif /* __CVC4__OPTIONS__${id}$_H */ +#endif /* CVC4__OPTIONS__${id}$_H */ diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp index a05ff63c3..c65e5da2a 100644 --- a/src/options/open_ostream.cpp +++ b/src/options/open_ostream.cpp @@ -2,9 +2,9 @@ /*! \file open_ostream.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h index b72c3a400..592db925f 100644 --- a/src/options/open_ostream.h +++ b/src/options/open_ostream.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__OPEN_OSTREAM_H -#define __CVC4__OPEN_OSTREAM_H +#ifndef CVC4__OPEN_OSTREAM_H +#define CVC4__OPEN_OSTREAM_H #include <map> #include <ostream> @@ -59,4 +59,4 @@ std::string cvc4_errno_failreason(); }/* CVC4 namespace */ -#endif /* __CVC4__OPEN_OSTREAM_H */ +#endif /* CVC4__OPEN_OSTREAM_H */ diff --git a/src/options/option_exception.cpp b/src/options/option_exception.cpp index 33e2e21d1..09bc94023 100644 --- a/src/options/option_exception.cpp +++ b/src/options/option_exception.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file option_exception.h +/*! \file option_exception.cpp ** \verbatim ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 63b8aa890..d337d4c9b 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -2,9 +2,9 @@ /*! \file option_exception.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__OPTION_EXCEPTION_H -#define __CVC4__OPTION_EXCEPTION_H +#ifndef CVC4__OPTION_EXCEPTION_H +#define CVC4__OPTION_EXCEPTION_H #include "base/exception.h" @@ -64,4 +64,4 @@ class CVC4_PUBLIC UnrecognizedOptionException : public CVC4::OptionException { }/* CVC4 namespace */ -#endif /* __CVC4__OPTION_EXCEPTION_H */ +#endif /* CVC4__OPTION_EXCEPTION_H */ diff --git a/src/options/options.h b/src/options/options.h index 1b61994c5..3f2d72b7e 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__OPTIONS__OPTIONS_H -#define __CVC4__OPTIONS__OPTIONS_H +#ifndef CVC4__OPTIONS__OPTIONS_H +#define CVC4__OPTIONS__OPTIONS_H #include <fstream> #include <ostream> @@ -560,4 +560,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__OPTIONS__OPTIONS_H */ +#endif /* CVC4__OPTIONS__OPTIONS_H */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 84b9f3b4c..7a4967de5 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -2,9 +2,9 @@ /*! \file options_handler.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Aina Niemetz + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -1245,6 +1245,45 @@ theory::bv::BvProofFormat OptionsHandler::stringToBvProofFormat( } } +const std::string OptionsHandler::s_bvOptimizeSatProofHelp = + "\ +Optimization levels currently supported by the --bv-optimize-sat-proof option:\n\ +\n\ + none : Do not optimize the SAT proof\n\ +\n\ + proof : Use drat-trim to shrink the SAT proof\n\ +\n\ + formula : Use drat-trim to shrink the SAT proof and formula (default)\ +"; + +theory::bv::BvOptimizeSatProof OptionsHandler::stringToBvOptimizeSatProof( + std::string option, std::string optarg) +{ + if (optarg == "none") + { + return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE; + } + else if (optarg == "proof") + { + return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF; + } + else if (optarg == "formula") + { + return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA; + } + else if (optarg == "help") + { + puts(s_bvOptimizeSatProofHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --bv-optimize-sat-proof: `") + + optarg + "'. Try --bv-optimize-sat-proof=help."); + } +} + + const std::string OptionsHandler::s_bitblastingModeHelp = "\ Bit-blasting modes currently supported by the --bitblast option:\n\ \n\ @@ -1769,10 +1808,11 @@ void OptionsHandler::proofEnabledBuild(std::string option, bool value) { #ifdef CVC4_PROOF if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER - && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT) + && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT + && options::bvSatSolver() != theory::bv::SAT_SOLVER_CRYPTOMINISAT) { throw OptionException( - "Eager BV proofs only supported when minisat is used"); + "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used"); } #else if(value) { @@ -1938,6 +1978,7 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("glpk", Configuration::isBuiltWithGlpk()); print_config_cond("cadical", Configuration::isBuiltWithCadical()); print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); + print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); print_config_cond("lfsc", Configuration::isBuiltWithLfsc()); print_config_cond("readline", Configuration::isBuiltWithReadline()); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 8b2629db7..06f7ab6e4 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -2,9 +2,9 @@ /*! \file options_handler.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Liana Hadarean + ** Tim King, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__OPTIONS__OPTIONS_HANDLER_H -#define __CVC4__OPTIONS__OPTIONS_HANDLER_H +#ifndef CVC4__OPTIONS__OPTIONS_HANDLER_H +#define CVC4__OPTIONS__OPTIONS_HANDLER_H #include <ostream> #include <string> @@ -148,6 +148,8 @@ public: theory::bv::BvProofFormat stringToBvProofFormat(std::string option, std::string optarg); + theory::bv::BvOptimizeSatProof stringToBvOptimizeSatProof(std::string option, + std::string optarg); theory::strings::ProcessLoopMode stringToStringsProcessLoopMode( std::string option, std::string optarg); @@ -238,6 +240,7 @@ public: static const std::string s_bitblastingModeHelp; static const std::string s_bvSatSolverHelp; static const std::string s_bvProofFormatHelp; + static const std::string s_bvOptimizeSatProofHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; static const std::string s_stringToStringsProcessLoopModeHelp; @@ -283,4 +286,4 @@ public: }/* CVC4::options namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__OPTIONS__OPTIONS_HANDLER_H */ +#endif /* CVC4__OPTIONS__OPTIONS_HANDLER_H */ diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h index 438d1c7cc..4cd77a441 100644 --- a/src/options/options_holder_template.h +++ b/src/options/options_holder_template.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__OPTIONS__OPTIONS_HOLDER_H -#define __CVC4__OPTIONS__OPTIONS_HOLDER_H +#ifndef CVC4__OPTIONS__OPTIONS_HOLDER_H +#define CVC4__OPTIONS__OPTIONS_HOLDER_H ${headers_module}$ @@ -35,4 +35,4 @@ struct OptionsHolder { } // namespace options } // namespace CVC4 -#endif /* __CVC4__OPTIONS__OPTIONS_HOLDER_H */ +#endif /* CVC4__OPTIONS__OPTIONS_HOLDER_H */ diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index d95335c76..39f2eb140 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 9650aba7a..1f7ba05fc 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -2,9 +2,9 @@ /*! \file options_template.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Mathias Preiner + ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -446,7 +446,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ smt2.6 | smtlib2.6 SMT-LIB format 2.6\n\ smt2.6.1 | smtlib2.6.1 SMT-LIB format 2.6 with support for the strings standard\n\ - tptp TPTP format (cnf and fof)\n\ + tptp TPTP format (cnf, fof and tff)\n\ sygus SyGuS format\n\ \n\ Languages currently supported as arguments to the --output-lang option:\n\ diff --git a/src/options/printer_modes.cpp b/src/options/printer_modes.cpp index 499646bbf..b60dde467 100644 --- a/src/options/printer_modes.cpp +++ b/src/options/printer_modes.cpp @@ -2,9 +2,9 @@ /*! \file printer_modes.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h index 456a7980b..79c57828b 100644 --- a/src/options/printer_modes.h +++ b/src/options/printer_modes.h @@ -2,9 +2,9 @@ /*! \file printer_modes.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__PRINTER__MODES_H -#define __CVC4__PRINTER__MODES_H +#ifndef CVC4__PRINTER__MODES_H +#define CVC4__PRINTER__MODES_H #include <iostream> @@ -45,4 +45,4 @@ std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC; }/* CVC4 namespace */ -#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */ +#endif /* CVC4__PRINTER__MODEL_FORMAT_H */ diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp index b08f71c2e..a1d012aa5 100644 --- a/src/options/quantifiers_modes.cpp +++ b/src/options/quantifiers_modes.cpp @@ -2,9 +2,9 @@ /*! \file quantifiers_modes.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index eea043865..c9aeda154 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__BASE__QUANTIFIERS_MODES_H -#define __CVC4__BASE__QUANTIFIERS_MODES_H +#ifndef CVC4__BASE__QUANTIFIERS_MODES_H +#define CVC4__BASE__QUANTIFIERS_MODES_H #include <iostream> @@ -316,4 +316,4 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mo }/* CVC4 namespace */ -#endif /* __CVC4__BASE__QUANTIFIERS_MODES_H */ +#endif /* CVC4__BASE__QUANTIFIERS_MODES_H */ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index d9d3e0d38..0a69178b3 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -456,6 +456,15 @@ header = "options/quantifiers_options.h" help = "interleave full saturate instantiation with other techniques" [[option]] + name = "fullSaturateStratify" + category = "regular" + long = "fs-stratify" + type = "bool" + default = "false" + read_only = true + help = "stratify effort levels in enumerative instantiation, which favors speed over fairness" + +[[option]] name = "literalMatchMode" category = "regular" long = "literal-matching=MODE" @@ -877,6 +886,15 @@ header = "options/quantifiers_options.h" help = "attempt to preprocess arbitrary inputs to sygus conjectures" [[option]] + name = "sygusAbduct" + category = "regular" + long = "sygus-abduct" + type = "bool" + default = "false" + read_only = false + help = "compute abductions using sygus" + +[[option]] name = "ceGuidedInst" category = "regular" long = "cegqi" @@ -1240,7 +1258,7 @@ header = "options/quantifiers_options.h" type = "bool" default = "false" read_only = true - help = "use sygus to enumerate and verify correctness of rewrite rules via sampling" + help = "use sygus to enumerate and verify correctness of rewrite rules" [[option]] name = "sygusRewSynth" @@ -1248,7 +1266,7 @@ header = "options/quantifiers_options.h" long = "sygus-rr-synth" type = "bool" default = "false" - help = "use sygus to enumerate candidate rewrite rules via sampling" + help = "use sygus to enumerate candidate rewrite rules" [[option]] name = "sygusRewSynthFilterOrder" @@ -1369,6 +1387,14 @@ header = "options/quantifiers_options.h" long = "sygus-expr-miner-check-timeout=N" type = "unsigned long" help = "timeout (in milliseconds) for satisfiability checks in expression miners" + +[[option]] + name = "sygusRewSynthRec" + category = "regular" + long = "sygus-rr-synth-rec" + type = "bool" + default = "false" + help = "synthesize rewrite rules over all sygus grammar types recursively" [[option]] name = "sygusQueryGen" @@ -1420,6 +1446,7 @@ header = "options/quantifiers_options.h" default = "false" help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" + [[option]] name = "sygusExprMinerCheckUseExport" category = "expert" @@ -1447,15 +1474,6 @@ header = "options/quantifiers_options.h" help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation" [[option]] - name = "recurseCbqi" - category = "regular" - long = "cbqi-recurse" - type = "bool" - default = "true" - read_only = true - help = "turns on recursive counterexample-based quantifier instantiation" - -[[option]] name = "cbqiSat" category = "regular" long = "cbqi-sat" diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp index c4690db36..dfdbb1ab7 100644 --- a/src/options/set_language.cpp +++ b/src/options/set_language.cpp @@ -2,9 +2,9 @@ /*! \file set_language.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Morgan Deters, Tim King, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/set_language.h b/src/options/set_language.h index ca691e9e5..0e3b32dd7 100644 --- a/src/options/set_language.h +++ b/src/options/set_language.h @@ -2,9 +2,9 @@ /*! \file set_language.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__OPTIONS__SET_LANGUAGE_H -#define __CVC4__OPTIONS__SET_LANGUAGE_H +#ifndef CVC4__OPTIONS__SET_LANGUAGE_H +#define CVC4__OPTIONS__SET_LANGUAGE_H #include <iostream> #include "options/language.h" @@ -96,4 +96,4 @@ std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_PUBLIC; }/* CVC4::language namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__OPTIONS__SET_LANGUAGE_H */ +#endif /* CVC4__OPTIONS__SET_LANGUAGE_H */ diff --git a/src/options/smt_modes.cpp b/src/options/smt_modes.cpp index 4a2fd404c..3501da878 100644 --- a/src/options/smt_modes.cpp +++ b/src/options/smt_modes.cpp @@ -2,9 +2,9 @@ /*! \file smt_modes.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/smt_modes.h b/src/options/smt_modes.h index 761f3be01..ed40a28a1 100644 --- a/src/options/smt_modes.h +++ b/src/options/smt_modes.h @@ -2,9 +2,9 @@ /*! \file smt_modes.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__SMT__MODES_H -#define __CVC4__SMT__MODES_H +#ifndef CVC4__SMT__MODES_H +#define CVC4__SMT__MODES_H #include <iosfwd> @@ -55,4 +55,4 @@ enum ModelCoresMode } // namespace CVC4 -#endif /* __CVC4__SMT__MODES_H */ +#endif /* CVC4__SMT__MODES_H */ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index e0041774a..3a3da2f14 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -297,6 +297,14 @@ header = "options/smt_options.h" help = "use aggressive extended rewriter as a preprocessing pass" [[option]] + name = "extRewPrepOnly" + category = "regular" + long = "ext-rew-prep-only" + type = "bool" + default = "false" + help = "use extended rewriter as the only preprocessing pass" + +[[option]] name = "simplifyWithCareEnabled" category = "regular" long = "simp-with-care" diff --git a/src/options/strings_process_loop_mode.h b/src/options/strings_process_loop_mode.h index 2933e034f..fb2248eec 100644 --- a/src/options/strings_process_loop_mode.h +++ b/src/options/strings_process_loop_mode.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H -#define __CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H +#ifndef CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H +#define CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H #include <iosfwd> @@ -52,4 +52,4 @@ std::ostream& operator<<(std::ostream& out, } // namespace CVC4 -#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */ +#endif /* CVC4__THEORY__BV__BITBLAST_MODE_H */ diff --git a/src/options/sygus_out_mode.h b/src/options/sygus_out_mode.h index 863e4d4bc..79480946a 100644 --- a/src/options/sygus_out_mode.h +++ b/src/options/sygus_out_mode.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -14,8 +14,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__SMT__SYGUS_OUT_MODE_H -#define __CVC4__SMT__SYGUS_OUT_MODE_H +#ifndef CVC4__SMT__SYGUS_OUT_MODE_H +#define CVC4__SMT__SYGUS_OUT_MODE_H #include <iosfwd> @@ -36,4 +36,4 @@ enum SygusSolutionOutMode } /* CVC4 namespace */ -#endif /* __CVC4__SMT__SYGUS_OUT_MODE_H */ +#endif /* CVC4__SMT__SYGUS_OUT_MODE_H */ diff --git a/src/options/theoryof_mode.cpp b/src/options/theoryof_mode.cpp index 59919a272..4d8d92e17 100644 --- a/src/options/theoryof_mode.cpp +++ b/src/options/theoryof_mode.cpp @@ -2,9 +2,9 @@ /*! \file theoryof_mode.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/theoryof_mode.h b/src/options/theoryof_mode.h index 0dc7194e9..900452fbc 100644 --- a/src/options/theoryof_mode.h +++ b/src/options/theoryof_mode.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h index fa7fad6be..d6a106ecf 100644 --- a/src/options/ufss_mode.h +++ b/src/options/ufss_mode.h @@ -2,9 +2,9 @@ /*! \file ufss_mode.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__BASE__UFSS_MODE_H -#define __CVC4__BASE__UFSS_MODE_H +#ifndef CVC4__BASE__UFSS_MODE_H +#define CVC4__BASE__UFSS_MODE_H namespace CVC4 { namespace theory { @@ -36,4 +36,4 @@ enum UfssMode{ }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__BASE__UFSS_MODE_H */ +#endif /* CVC4__BASE__UFSS_MODE_H */ |