Instead of asserting theory axioms lazily we create them on the fly and allow propagation eagerly.
The approach uses a waterfall model as follows:
- terms are created: they are inserted into an index for (set.in x S) axiom creation.
- two terms are merged by an equality.
Loop over all new opportunities for axiom instantiation
New axioms are added to a queue of recently created axioms.
- an atomic formula was asserted by the SAT solver.
Update the watch list to find new propagations.
During propagation recently created axioms are either inserted into a propagation queue, or inserted into a watch list.
They are inserted into a propagation queue all or all but one literal is assigned to false.
They are inserted into a watch list if at least two literals are unassigned
They are dropped if the axiom contains a literal that is assigned to true
The propagation queue is processed by by asserting the theory axiom to the core.
Also add some elementary statistics.
A breaking change is to change the datatype for undo-trail in smt_context to not use a custom data-structure.
This can likely cause regressions. For example, the region allocator now comes from the stack_trail instead of being
owned within smt_context with a different declaration order. smt_context could crash during destruction or maybe even pop.
We take the risk as the change is overdue.
Add swap method to ref_vector.
* Initial plan
* Implement theory_finite_set header and implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add theory registration to smt_setup
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update theory_finite_set.cpp
* Refactor membership_atoms and add elements list
Renamed membership_atoms to membership_elements and added elements list.
* Change membership elements to use enode type
* Update theory_finite_set.cpp
* Fix typo in internalize_atom function
* Update theory_finite_set.cpp
* Refactor final_check_eh by removing comments
Removed redundant comments and cleaned up code.
* Add m_lemmas member to theory_finite_set class
* Improve clause management and instantiation logic
Refactor clause handling and instantiate logic in finite set theory.
* Add friend class declaration for testing
* Add placeholder methods for lemma instantiation
Added placeholder methods for lemma instantiation.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Add commands:
(prefer <formula>)
- will instruct case split queue to assign formula to true.
- prefer commands added within a scope are forgotten after leaving the scope.
(reset-preferences)
- resets asserted preferences. Has to be invoked at base level.
This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2
for equations x*y + z = 0,
with x, y, z integer, enforce that x divides z
It is (currently) enabled within Grobner completion
and applied partially to x a variable, z linear, and
only when |z| < |x|.
