* Initial plan
* Add support for ARM to X64 cross-compilation on macOS
- Initialize LINUX_X64 from mk_util.LINUX_X64
- Add support for --arch=x64 flag to force x64 builds
- Handle cross-compilation from ARM64 to x64 on macOS using -arch x86_64 flags
- Update help text to reflect both arm64 and x64 architecture options
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix cross-compilation detection using HOST_IS_ARM64
Use separate HOST_IS_ARM64 variable to track the host architecture,
allowing proper detection of ARM to x64 cross-compilation scenarios.
This ensures the correct compiler flags are set when building x64
on ARM hosts.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Address code review: improve arch flag handling
- Extract target_arch_flag to variable to reduce duplication
- Add .strip() calls to handle trailing spaces in environment variables
- Ensure proper spacing in concatenated flags
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Update cross-build workflow to use g++-12 for C++20 support
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* restore more aggressive pruning in search tree
* restore where we close children to be correct
* add core strengthening check
* fix recursion bug
* less strict core propagation
* old search tree version
* restore search tree patch
* remove flag
* debugging inconsistent end state with search, some changes need to be made in search tree, only backtrack should be closing nodes, I think the bug is when we do find_highest_attach for nonchronological backjumping, you might get to a point where the sibling is closed, so then we need to resolve further up the tree
* clean up code, fix deadlock
* delete test files
* clean up
---------
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
* restore more aggressive pruning in search tree
* restore where we close children to be correct
* add core strengthening check
* fix recursion bug
* less strict core propagation
* old search tree version
* restore search tree patch
* remove flag
---------
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
* Initial plan
* Update ARM GCC toolchain from 11.2 to 13.3 for C++20 std::format support
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* somewhaat failed attempt at declaring subterm predicate
I can't really figure out how to link the smt parser to the rest of the
machinenery, so I will stop here and try from the other side. I'll start
implmenting the logic and see if it brings me back to the parser.
* initial logic implmentation
Very primitive, but I don't like have that much work uncommitted.
* parser implementation
* more theory
* Working base
* subterm reflexivity
* a few optimization
Skip adding obvious equalities or disequality
* removed some optimisations
* better handling of backtracking
* stupid segfault
Add m_subterm to the trail
* Update src/smt/theory_datatype.h
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
* Update src/ast/rewriter/datatype_rewriter.cpp
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
* Update src/smt/theory_datatype.cpp
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
* Update src/smt/theory_datatype.cpp
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
* Update src/smt/theory_datatype.cpp
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
* review
* forgot to update `iterate_subterm`'s signature
* fix iterator segfault
* Remove duplicate include statement
Removed duplicate include of 'theory_datatype.h'.
* Replace 'optional' with 'std::option' in datatype_decl_plugin.h
* Add is_subterm_predicate matcher to datatype_decl_plugin
* Change std::option to std::optional for m_subterm
* Update pdecl.h
* Change has_subterm to use has_value method
* Update pdecl.cpp
---------
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
