I have an AIG (and-inverter graph) which I keep modifying and whose satisfiability I need to check in an incremental manner using Z3. I can generate a CNF representation of the AIG and would ideally like to feed these clauses directly to the solver and call it repeatedly from my code. Is there some way that I can directly add clauses (or an AIG) to Z3 solver through C/C++ APIs?
1
There are 1 best solutions below
Related Questions in C++
- How to know a Pod's own IP address from inside a container in the Pod?
- Who will decide the "specified number of pods" for replication controller in kubernetes?
- Access other containers of a pod in Kubernetes
- Kubernetes cluster using Vagrant not working after restart
- kubectl not installed with gcloud SDK
- How do I access the Kubernetes api from within a pod container?
- Exposing several services with Vagrant and Kubernetes on my own server
- Does Kubernetes provision new VMs for pods on my cloud platform?
- Any suggestion for running Aerospike on Kubernetes on CoreOS on GCE?
- Kubernetes - kubectl exec bash - session drop and line width
Related Questions in C
- How to know a Pod's own IP address from inside a container in the Pod?
- Who will decide the "specified number of pods" for replication controller in kubernetes?
- Access other containers of a pod in Kubernetes
- Kubernetes cluster using Vagrant not working after restart
- kubectl not installed with gcloud SDK
- How do I access the Kubernetes api from within a pod container?
- Exposing several services with Vagrant and Kubernetes on my own server
- Does Kubernetes provision new VMs for pods on my cloud platform?
- Any suggestion for running Aerospike on Kubernetes on CoreOS on GCE?
- Kubernetes - kubectl exec bash - session drop and line width
Related Questions in Z3
- How to know a Pod's own IP address from inside a container in the Pod?
- Who will decide the "specified number of pods" for replication controller in kubernetes?
- Access other containers of a pod in Kubernetes
- Kubernetes cluster using Vagrant not working after restart
- kubectl not installed with gcloud SDK
- How do I access the Kubernetes api from within a pod container?
- Exposing several services with Vagrant and Kubernetes on my own server
- Does Kubernetes provision new VMs for pods on my cloud platform?
- Any suggestion for running Aerospike on Kubernetes on CoreOS on GCE?
- Kubernetes - kubectl exec bash - session drop and line width
Related Questions in SAT
- How to know a Pod's own IP address from inside a container in the Pod?
- Who will decide the "specified number of pods" for replication controller in kubernetes?
- Access other containers of a pod in Kubernetes
- Kubernetes cluster using Vagrant not working after restart
- kubectl not installed with gcloud SDK
- How do I access the Kubernetes api from within a pod container?
- Exposing several services with Vagrant and Kubernetes on my own server
- Does Kubernetes provision new VMs for pods on my cloud platform?
- Any suggestion for running Aerospike on Kubernetes on CoreOS on GCE?
- Kubernetes - kubectl exec bash - session drop and line width
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
Popular # Hahtags
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
Yes, you can simply assert new assertions, which are internally translated into clauses.
Note that for many incremental solving problems, Z3 does not use an off-the-shelf, dedicated SAT-solver, but it's own SMT solver that incorporates some of the features of SAT solvers, but not all, and which natively handles non-Boolean problems. So, it's not necessarily the case that hacking the solver to inject clauses directly will translate into significantly improved performance.
Z3 also has a dedicated Boolean-only SAT solver and if you're solving purely Boolean problems, this solver is likely much faster. You can force it to use this solver by replacing
(check-sat)with(check-sat-using sat), or by running the tactic called 'sat'. The implementation of this solver is in sat_solver.h/.cpp, which would be the prime place to start looking around, if you'd like to hack it.Z3 also uses it's own implementation of AIGs as a pre-processing step in some tactics, see aig_tactic.h/.cpp.