summaryrefslogtreecommitdiff
path: root/src/theory/booleans
AgeCommit message (Collapse)Author
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
2021-02-24Enable -Werror. (#5969)Mathias Preiner
2020-12-08[proof-new] Updating SAT proof to use MACRO_RESOLUTION (#5613)Haniel Barbosa
2020-12-07[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)Haniel Barbosa
Previously CHAIN_RESOLUTION's definition and checker were not properly capturing its intended behavior as merely an n-ary RESOLUTION rule (i.e., no factoring nor reordering). A new rule, MACRO_RESOLUTION, now captures this behavior: it combines CHAIN_RESOLUTION, FACTORING, and REORDERING. This commit also adds a proof checker for the new rule and updates the proof checker of CHAIN_RESOLUTION.
2020-12-02Update copyright headers.Aina Niemetz
2020-10-21(proof-new) Make circuit propagator proof producing (#5318)Gereon Kremer
This PR uses the proofs from #5301 to actually produce proofs from the circuit propagator.
2020-10-20(proof-new) Add proofs for circuit propagator (#5301)Gereon Kremer
This PR adds code to generate proofs for inferences within the (non-clausal) circuit propagator. It consists of many small methods that each implement simple derivations about single Boolean connectives. It uses already existing proof rules, and thus no separate proof checker is required. A second PR will use these rules within the circuit propagator class.
2020-10-19[proof-new] Fixing resolution proof checker (#5262)Haniel Barbosa
Previously the binary resolution checker was: - Checking applications in which for a pivot (not l) the literal (not l) would be eliminated from the first clause and l from the second because double negation was handled implicitly. Now whether the binary resolution is such that the pivot is removed as is from the first clause and negated from the second, or the other way around, is marked via an argument. - Not producing false the remaining set of literals after resolution was empty. This commit also updates the informal description of the rule accordingly, as well as to clarify the behavior when the pivot does not occur properly in the clauses (in which case the rule application corresponds to weakening). Co-authored-by: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
2020-10-13(proof-new) New rules for Booleans (#5243)Andrew Reynolds
This adds 2 new rules for convenience to the Boolean checker.
2020-10-06(proof-new) Add interface for trusted substitution and update ppAssert (#5193)Andrew Reynolds
The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions. This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface. This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-09-16[proof-new] Resolution rules and checkers (#5070)Haniel Barbosa
2020-07-13 (proof-new) SMT Preprocess proof generator (#4708)Andrew Reynolds
This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine. It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.
2020-07-10(proof-new) Update Theory interface for proof-new (#4648)Andrew Reynolds
This includes 4 changes: Theory constructor takes a ProofNodeManager, Theory::explain returns a TrustNode (of kind PROP_EXP), Theory::expandDefinitions returns a TrustNode (of kind REWRITE), Theory::ppRewrite returns a TrustNode (of kind REWRITE). These are all currently planned updates to the interface of Theory. This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support. This PR is also contingent on the performance tests for proof-new on SMT-LIB.
2020-06-19Always rewrite boolean ITEs with constant then/else-branches (#4619)Haniel Barbosa
Also adds better tracing and rewrites for binary AND/OR to account for reductions from constant ITEs. An evaluation of master vs this commit, with 600s, no options, shows the impact of this commit to be negligible and mostly restricted to QF_LIA. Below there is a summary and a list of the unique solves. ``` Benchmark | Stat Slvd Tot To Mo Err Cpu[s] Mem[MB] Uniq | Stat Slvd Tot To Mo Err Cpu[s] Mem[MB] Uniq | QF_ALIA | ok 125 126 1 0 0 2382.6 5410.8 0 | ok 125 126 1 0 0 2322.1 5211.8 0 | QF_AX | ok 549 551 2 0 0 2381.4 2533.1 0 | ok 549 551 2 0 0 2400.8 2676.4 0 | QF_IDL | ok 1682 2193 511 0 0 399395.4 491490.3 3 | ok 1682 2193 511 0 0 400813.9 491129.9 3 | QF_LIA | ok 4419 6947 2521 7 0 1774140.9 2782838.1 27 | ok 4409 6947 2531 7 0 1775886.7 2785165.7 17 | QF_LIRA | ok 5 7 2 0 0 1209.9 3626.9 0 | ok 5 7 2 0 0 1209.5 3707.2 0 | QF_LRA | ok 1517 1648 131 0 0 134215.1 170443.1 3 | ok 1516 1648 132 0 0 134819.6 169942.7 2 | QF_RDL | ok 210 255 45 0 0 32896.0 23261.0 0 | ok 210 255 45 0 0 32902.7 23312.5 0 | QF_UF | ok 7444 7457 13 0 0 16156.4 74432.9 0 | ok 7444 7457 13 0 0 16043.8 75067.6 0 | __totals | ok 15951 19184 3226 7 0 2362777.7 3554036.2 33 | ok 15940 19184 3237 7 0 2366399.2 3556213.8 22 |``` ``` DIRECTORY | master | branch | Benchmark | Stat RES Exit Cpu[s] Mem[MB] | Stat RES Exit Cpu[s] Mem[MB] | non_incremental_QF_IDL/asp-GraphPartitioning-rand_21_150_1235870252_0_k=3_v=10_e=20_unsat.gph.smt2 | to - 2 600.1 246.4 | ok 20 0 596.71 245.9 | non_incremental_QF_IDL/asp-SchurNumbers-15.13.schur.lp.smt2 | ok 10 0 533.64 243.8 | to - 2 600.07 246.8 | non_incremental_QF_IDL/job_shop-jobshop38-2-19-19-4-4-12.smt2 | ok 10 0 586.13 221.5 | to - 2 600.09 216.8 | non_incremental_QF_IDL/queens_bench-n_queen-queen82-1.smt2 | to - 2 600.01 197.8 | ok 10 0 570.36 198.9 | non_incremental_QF_IDL/schedulingIDL-tai_15x15_3_mkspan871.smt2 | to - 2 600.1 128.0 | ok 10 0 586.8 127.8 | non_incremental_QF_IDL/schedulingIDL-tai_15x15_9_mkspan930.smt2 | ok 10 0 575.55 124.4 | to - 2 600.07 122.6 | non_incremental_QF_LIA/arctic-matrix-constraint-1007795.smt2 | ok 10 0 334.96 386.7 | to - 2 600.02 335.5 | non_incremental_QF_LIA/arctic-matrix-constraint-1008025.smt2 | ok 10 0 180.57 384.6 | to - 2 600.02 338.6 | non_incremental_QF_LIA/arctic-matrix-constraint-1107622.smt2 | ok 10 0 310.68 349.2 | to - 2 600.01 341.3 | non_incremental_QF_LIA/arctic-matrix-constraint-1275621.smt2 | ok 10 0 5.59 232.0 | to - 2 600.04 407.4 | non_incremental_QF_LIA/arctic-matrix-constraint-1360077.smt2 | ok 10 0 422.4 667.7 | to - 11 591.94 663.2 | non_incremental_QF_LIA/arctic-matrix-constraint-1765766.smt2 | to - 11 598.02 656.8 | ok 10 0 62.5 669.8 | non_incremental_QF_LIA/arctic-matrix-constraint-391798.smt2 | ok 10 0 9.0 119.3 | to - 2 600.08 131.8 | non_incremental_QF_LIA/arctic-matrix-constraint-481231.smt2 | ok 10 0 402.37 220.9 | to - 2 600.09 199.6 | non_incremental_QF_LIA/arctic-matrix-constraint-689472.smt2 | ok 10 0 28.51 155.9 | to - 2 600.06 215.1 | non_incremental_QF_LIA/arctic-matrix-constraint-864173.smt2 | ok 10 0 125.59 326.3 | to - 11 597.87 348.8 | non_incremental_QF_LIA/arctic-matrix-constraint-901628.smt2 | to - 2 600.04 225.5 | ok 10 0 391.31 228.3 | non_incremental_QF_LIA/arctic-matrix-constraint-916576.smt2 | to - 2 600.01 244.4 | ok 10 0 432.4 246.9 | non_incremental_QF_LIA/arctic-matrix-constraint-928134.smt2 | ok 10 0 447.55 222.7 | to - 2 600.06 264.7 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-42.smt2 | ok 10 0 579.39 414.9 | to - 2 600.07 417.4 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-47.smt2 | to - 2 600.02 604.2 | ok 10 0 594.54 603.6 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-45-43.smt2 | to - 2 600.05 628.1 | ok 10 0 588.25 627.6 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-46-47.smt2 | ok 10 0 589.88 570.0 | to - 2 600.09 566.9 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-47.smt2 | ok 20 0 590.89 599.9 | to - 2 600.01 598.4 | non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-50.smt2 | ok 10 0 594.72 804.7 | to - 11 593.13 843.5 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-17-47.smt2 | ok 20 0 593.29 524.2 | to - 2 600.08 522.8 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-20-48.smt2 | to - 2 600.02 562.5 | ok 10 0 594.33 560.3 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-5-46.smt2 | to - 2 600.09 492.9 | ok 10 0 576.02 491.9 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-52-47.smt2 | to - 2 600.02 532.2 | ok 20 0 592.3 533.4 | non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-53-48.smt2 | ok 20 0 599.82 729.4 | to - 2 600.02 742.1 | non_incremental_QF_LIA/nec-smt-large-getoption_user-prp-41-47.smt2 | to - 11 589.46 1377.2 | ok 20 0 580.82 1380.1 | non_incremental_QF_LIA/nec-smt-large-user_is_in_group-prp-23-46.smt2 | to - 2 600.08 633.5 | ok 10 0 576.07 634.0 | non_incremental_QF_LIA/tropical-matrix-constraint-1015084.smt2 | ok 10 0 408.08 374.5 | to - 2 600.01 336.4 | non_incremental_QF_LIA/tropical-matrix-constraint-1206577.smt2 | ok 10 0 361.82 375.4 | to - 11 593.45 288.4 | non_incremental_QF_LIA/tropical-matrix-constraint-1268455.smt2 | ok 10 0 270.87 654.3 | to - 2 600.08 670.5 | non_incremental_QF_LIA/tropical-matrix-constraint-1270163.smt2 | to - 2 600.02 410.4 | ok 10 0 425.02 420.6 | non_incremental_QF_LIA/tropical-matrix-constraint-1270998.smt2 | ok 10 0 349.91 384.6 | to - 2 600.01 417.5 | non_incremental_QF_LIA/tropical-matrix-constraint-1290859.smt2 | to - 2 600.1 365.9 | ok 10 0 117.77 270.0 | non_incremental_QF_LIA/tropical-matrix-constraint-1361831.smt2 | to - 2 600.07 431.0 | ok 10 0 421.55 686.9 | non_incremental_QF_LIA/tropical-matrix-constraint-1452366.smt2 | to - 2 600.04 439.4 | ok 10 0 87.42 451.9 | non_incremental_QF_LIA/tropical-matrix-constraint-1791895.smt2 | to - 2 600.1 480.3 | ok 10 0 102.16 459.7 | non_incremental_QF_LIA/tropical-matrix-constraint-1908553.smt2 | to - 2 600.01 713.8 | ok 10 0 22.22 394.9 | non_incremental_QF_LIA/tropical-matrix-constraint-2061672.smt2 | ok 10 0 51.6 521.2 | to - 2 600.04 545.8 | non_incremental_QF_LIA/tropical-matrix-constraint-244431.smt2 | ok 10 0 292.95 88.2 | to - 2 600.01 97.7 | non_incremental_QF_LIA/tropical-matrix-constraint-368069.smt2 | to - 2 600.05 135.3 | ok 10 0 445.93 134.2 | non_incremental_QF_LIA/tropical-matrix-constraint-369883.smt2 | ok 10 0 510.59 134.2 | to - 2 600.01 127.7 | non_incremental_QF_LIA/tropical-matrix-constraint-527358.smt2 | ok 10 0 243.33 135.0 | to - 2 600.05 140.7 | non_incremental_QF_LIA/tropical-matrix-constraint-614657.smt2 | ok 10 0 515.89 209.6 | to - 2 600.07 166.6 | non_incremental_QF_LIA/tropical-matrix-constraint-645054.smt2 | ok 10 0 41.34 185.3 | to - 2 600.08 205.1 | non_incremental_QF_LIA/tropical-matrix-constraint-794687.smt2 | ok 10 0 502.03 235.3 | to - 2 600.07 242.0 | non_incremental_QF_LRA/LassoRanker-CooperatingT2-sas2.t2.c_Iteration7_Loop_7-phaseTemplate.smt2 | ok 20 0 593.7 591.3 | to - 2 600.03 614.7 | non_incremental_QF_LRA/LassoRanker-SV-COMP-aviad_true-termination.c_Iteration1_Loop_4-phaseTemplate.smt2 | ok 10 0 594.16 738.5 | to - 2 600.03 701.6 | non_incremental_QF_LRA/LassoRanker-Ultimate-Collatz.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | to - 2 600.09 711.5 | ok 20 0 593.46 711.2 | non_incremental_QF_LRA/tropical-matrix-constraint-199552.smt2 | ok 10 0 268.04 71.2 | to - 2 600.05 81.6 | non_incremental_QF_LRA/tropical-matrix-constraint-223827.smt2 | to - 2 600.06 91.9 | ok 10 0 505.07 95.9 |```
2020-06-16Update copyright headers.Aina Niemetz
2020-06-03(proof-new) Adding rules and proof checker for Boolean reasoning (#4560)Haniel Barbosa
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
This commit adds statistics for string rewrites. This is work towards proof support in the string solver. At a high level, this commit adds a pointer to a `SequenceStatistics` in the rewriters and modifies `SequencesRewriter::returnRewrite()` to count the rewrites done. In practice, to make this work requires a couple of changes, some of them temporary: - We can't have a single `Rewriter` instance shared between different `SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the `SmtEngine` and calling the rewriter retrieves the rewriter associated with the current `SmtEngine`. This is a temporary workaround before we get rid of singletons. - Methods in the `SequencesRewriter` and the `StringsRewriter` are made non-`static` because they need access to the statistics instance. - `StringsEntail` now has non-`static` methods because it needs a reference to the sequences rewriter that it can call. - The interaction between the `StringsRewriter` and the `SequencesRewriter` changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits from `SequencesRewriter` and calls its `postRewrite()` before applying its own rewrites (this is essentially a reversal of roles from before: the `SequencesRewriter` used to call `static` methods in the `StringsRewriter`). - The theory rewriters are now owned by the individual theories. This design mirrors the `EqualityEngine`s owned by the individual theories.
2020-04-01Initialize theory rewriters in theories (#4197)Andres Noetzli
Until now, the `Rewriter` was responsible for creating `TheoryRewriter` instances. This commit adds a method `mkTheoryRewriter()` that theories override to create an instance of their corresponding theory rewriter. The advantage is that the theories can pass additional information to their theory rewriter (e.g. a statistics object).
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-24Make lambda rewriter more robust (#3806)Andres Noetzli
The lambda rewriter was not robust to the case where the lambda of the array representation contained a disequality, e.g. `not(x = 1))`. It would process it as `ite(not(x = 1), true, false)` instead of `ite(x = 1, false, true)`, which meant that it wasn't able to turn it into an array representation when checking const-ness. Additionally, the rewriter had issues when the lambda was of the form `ite((= x c1), true, (= y c2))` (after turning it into an array and then into a lambda) because it is expecting the false branch of the `ite` to not contain `y` variables, making it non-constant despite the array being constant. This commit solves that issue by normalizing `ite(not(c), x, y) ---> ite(c, y, x)`.
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
This commit changes theory rewriters to be non-static. This refactoring is needed as a stepping stone to making our rewriter configurable: If we have multiple solver objects with different rewrite configurations, we cannot use `static` variables for the rewriter table in the BV rewriter for example. It is also in line with our goal of getting rid of singletons in general. Note that the `Rewriter` class is still a singleton, which will be changed in a future commit.
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-22NodeValue: Eliminate redundant NBITS macros. (#3400)Aina Niemetz
Previously, the metakind header defined macros for the number of bits reserved for fields in the NodeValue "header" (for the reference count, the node kind, the number of children and the node id). These macros were redundant, since the only one using them was the NodeValue itself, which redefined them (while using them) as constants in the class. Additionally, MAX_CHILDREN was defined (using these macros) not only in the metakind header, but redefined in other places. This commit defines the above values as constexpr members of the NodeValue class and cleans up redundancy.
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-09-22cmake: Remove unused CMakeLists.txtMathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-04Transfer ownership of learned literals from SMT engine to circuit ↵Aina Niemetz
propagator. (#2421)
2018-08-28Reorder circuit propagator class.Aina Niemetz
2018-08-28Move flag needsFinish from SMT engine to circuit propagator.Aina Niemetz
2018-08-28Solve equalities between Boolean variables in presolve. (#2390)Andrew Reynolds
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-07Fixing more inconsistent usages of override. (#1575)Tim King
2018-01-10Removing throw specifiers for TypeRules. (#1501)Tim King
2018-01-10Removing throw specifiers from type enumerators. (#1502)Tim King
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes.
2017-07-07Update copyright headers.Mathias Preiner
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge ↵Tim King
commit for nlAlgMaster.
2017-03-27Remove throw qualifiers in type enumeratorsAndres Notzli
This addresses Coverity issues: - 1172154 - 1172156 - 1172157 - 1172158 - 1172159 - 1379612 - 1379612 - 1421430 - 1172166 - 1172144 - 1362709 - 1362696 - 1172145 - 1172147 - 1172148 - 1379610 - 1362772 - 1362676 - 1362704 - 1362749 - 1362876 - 1362843 - 1362837 - 1362881 - 1172223 - 1172155
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2016-10-19Fix minor bug and typo in boolean rewriterfix_rewriteAndres Notzli
One of the rewrites in the boolean rewriter had the condition `n[0] == tt && n[0] == ff`, which could never be true. Another rewrite covers the same case but returns a `REWRITE_AGAIN` instead of a `REWRITE_DONE`. This commit also fixes a minor typo.
2016-04-20update from the masterPaulMeng
2016-01-28Adding listeners to Options.Tim King
- Options -- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options. -- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners. -- Added functions to Options for registering listeners of the notify calls. -- Changed a number of options to use the new listener infrastructure. -- Fixed a number of warnings in options. -- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure. -- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}. - Theories -- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options. - Ostream Handling: -- Added new functionality that generalized how ostreams are opened, options/open_stream.h. -- Simplified the memory management for different ostreams, smt/managed_ostreams.h. -- Had the SmtEnginePrivate manage the memory for the ostreams set by options. -- Simplified how the setting of ostreams are updated, smt/update_ostream.h. - Configuration and Tags: -- Configuration can now be used during predicates and handlers for options. -- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/. -- Moved {Debug,Trace}_tags.* from being generated in options/ into base/. - cvc4_private.h -- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's. -- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations. -- Made lib/lib/clock_gettime.h a cvc4_private_library.h header. - Antlr -- Fixed antlr and cvc4 macro definition conflicts that caused warnings. - SmtGlobals -- Refactored replayStream and replayLog out of SmtGlobals. -- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
2016-01-15Type enumerators take optional argument indicating fixed cardinalities of ↵ajreynol
uninterpreted sorts. Modify TheoryModelBuilder. Fix bug in fmf-empty-sorts.
2016-01-05Add SmtGlobals ClassTim King
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library. - The option replayLog has been removed due to inconsistent memory management. - SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently. - There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine. - A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction. - Selected classes have been given a copy of this pointer in their constructors. - Removed the dependence on Node from Result. Moving Result back into util/.
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
What to Know As a User: A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems. The Problem: The build order of CVC4 used to be [roughly] specified as: options < expr < util < libcvc4 < parsers < main Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable. The Solution: To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen: 1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file. 2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options. 3. All of the old options_handlers.h files have been refactored. 4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary. 5. I am removing the libstatistics library. The constraints that the CVC4 build system will eventually satisfy are: - The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files. - The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases. - The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.) - One library per Makefile.am. - No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.) The build order of CVC4 can now be [roughly] specified as base < options < util < expr < smt_util < libcvc4 < parsers < main The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean. More details about the directories: base/ The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere. options/ The options/ directory is self contained. - It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h . - There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options. - Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done. - The */options_handlers.h files have been removed. - The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp. - All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h . util/ The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean. expr/ The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/. - An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h. - Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h. - The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/. - Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes. - Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources. - This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC. smt_util/ The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel. What is up next: - A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed. - The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback