YuhangQ/ACEC
1
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

inital commit

Browse Source
This commit is contained in:
YuhangQ 2022-10-14 14:04:57 +08:00
parent f983cfca36
commit 03691a7e97
19 changed files with 4047 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.gitignore vendored
View File

@ -30,3 +30,7 @@
*.exe
*.out
*.app
acec
amulet2
build

6
.vscode/settings.json vendored Normal file
View File

@ -0,0 +1,6 @@
{
"files.associations": {
"*.ejs": "html",
"iostream": "cpp"
}
}

147
acec.cpp Normal file
View File

@ -0,0 +1,147 @@
#include <bits/stdc++.h>
#include "vec.hpp"
#include "circuit.hpp"
#include "sweep.hpp"
#include "libopenf4.h"
extern "C" {
#include "aiger.h"
}
#define pvar(i) ((string((i) < 0 ? "N" : "") + "A" + std::to_string(abs(i))).c_str())
Sweep* sweep_init(int argv, char* args[]) {
Sweep *S = new Sweep();
S->aig = aiger_init();
S->det_v_sz = 0;
S->file = fopen(args[1], "r");
return S;
}
int main(int argv, char* args[]) {
Sweep *S = sweep_init(argv, args);
S->solve();
using namespace std;
//using namespace F4;
// Create polynomial array.
vector<string> polynomialArray;
// Create variable name array.
vector<string> variableName;
set<string> vars;
int t = S->maxvar;
for (int i = 1; i <= S->maxvar; i++) {
circuit *c = &(S->C[i]);
if (!c->sz || S->del[i] == 2) continue;
if(c->type == And) {
char term[1024];
sprintf(term, "-%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->to[0]));
for(int i=1; i<c->sz; i++) {
sprintf(term, "%s*%s", term, pvar(c->to[i]));
}
polynomialArray.push_back(term);
printf("%s\n", term);
}
if(c->type == Xor) {
string last = pvar(c->to[0]);
char term[1024];
for(int i=1; i<c->sz-1; i++) {
string tmp = pvar(++t);
sprintf(term, "-%s-2*%s*%s+%s+%s", tmp.c_str(), last.c_str(), pvar(c->to[i]), last.c_str(), pvar(c->to[i]));
polynomialArray.push_back(term);
printf("%s\n", term);
last = tmp;
}
sprintf(term, "-%s-2*%s*%s+%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), last.c_str(), pvar(c->to[c->sz-1]), last.c_str(), pvar(c->to[c->sz-1]));
polynomialArray.push_back(term);
printf("%s\n", term);
}
if (c->type == HA || c->type == FA) {
char term[1024];
sprintf(term, "-%s-2*%s+%s", pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->carrier), pvar(c->to[0]));
for(int i=1; i<c->sz; i++) {
sprintf(term, "%s+%s", term, pvar(c->to[i]));
}
polynomialArray.push_back(term);
printf("%s\n", term);
}
if(c->type == Majority) {
char term[1024];
sprintf(term, "-%s-2*%s+%s", pvar(++t), pvar(i * (S->C[i].neg ? -1 : 1)), pvar(c->to[0]));
for(int i=1; i<c->sz; i++) {
sprintf(term, "%s+%s", term, pvar(c->to[i]));
}
polynomialArray.push_back(term);
printf("%s\n", term);
}
// if (c->type == HA || c->type == FA) {
// printf("( %d %d )", i * (S->C[i].neg ? -1 : 1), c->carrier);
// }
// else {
// printf("%d", i * (S->C[i].neg ? -1 : 1));
// }
// printf(" = %s ( ", gate_type[c->type].c_str());
// for (int j = 0; j < c->sz; j++) {
// printf("%d ", c->to[j]);
// }
// puts(")");
}
for(int i=t; i>=1; i--) {
variableName.push_back(pvar(i));
variableName.push_back(pvar(-i));
char term[1024];
sprintf(term, "-%s+%s^2", pvar(i), pvar(i));
polynomialArray.emplace_back(term);
printf("%s\n", term);
sprintf(term, "%s+%s", pvar(i), pvar(-i));
polynomialArray.emplace_back(term);
printf("%s\n", term);
}
char term[1024];
sprintf(term, "-%s+1", pvar(S->maxvar));
polynomialArray.emplace_back(term);
printf("%s\n", term);
// for(int i = 0; i < 6; i++)
// {
// variableName.push_back('x'+to_string(i));
// }
// // Fill the polynomial array.
// polynomialArray.emplace_back("x0+x1+x2+x3+x4+x5");
// polynomialArray.emplace_back("x0*x1+x1*x2+x2*x3+x3*x4+x0*x5+x4*x5");
// polynomialArray.emplace_back("x0*x1*x2+x1*x2*x3+x2*x3*x4+x0*x1*x5+x0*x4*x5+x3*x4*x5");
// polynomialArray.emplace_back("x0*x1*x2*x3+x1*x2*x3*x4+x0*x1*x2*x5+x0*x1*x4*x5+x0*x3*x4*x5+x2*x3*x4*x5");
// polynomialArray.emplace_back("x0*x1*x2*x3*x4+x0*x1*x2*x3*x5+x0*x1*x2*x4*x5+x0*x1*x3*x4*x5+x0*x2*x3*x4*x5+x1*x2*x3*x4*x5");
// polynomialArray.emplace_back("x0*x1*x2*x3*x4*x5-1");
// Compute a reduce groebner basis.
vector<string> basis = groebnerBasisF4(7, variableName.size(), variableName, polynomialArray, 1, 0);
for(size_t i = 0; i < basis.size(); i++)
{
cout << basis[i] << endl;
}
for(int i=t; i>=1; i--) {
printf("(declare-fun %s () Bool)", pvar(i));
printf("(declare-fun %s () Bool)", pvar(-i));
}
return 0;
}

2775
aiger.c Normal file
View File

File diff suppressed because it is too large Load Diff

359
aiger.h Normal file
View File

@ -0,0 +1,359 @@
/***************************************************************************
Copyright (c) 2006 - 2018, Armin Biere, Johannes Kepler University.
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to
deal in the Software without restriction, including without limitation the
rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
IN THE SOFTWARE.
***************************************************************************/
/*------------------------------------------------------------------------*/
/* This file contains the API of the 'AIGER' library, which is a reader and
* writer for the AIGER AIG format. The code of the library
* consists of 'aiger.c' and 'aiger.h'. It is independent of 'simpaig.c'
* and 'simpaig.h'.
* library.
*/
#ifndef aiger_h_INCLUDED
#define aiger_h_INCLUDED
#include <stdio.h>
/*------------------------------------------------------------------------*/
#define AIGER_VERSION "1.9"
/*------------------------------------------------------------------------*/
typedef struct aiger aiger;
typedef struct aiger_and aiger_and;
typedef struct aiger_symbol aiger_symbol;
/*------------------------------------------------------------------------*/
/* AIG references are represented as unsigned integers and are called
* literals. The least significant bit is the sign. The index of a literal
* can be obtained by dividing the literal by two. Only positive indices
* are allowed, which leaves 0 for the boolean constant FALSE. The boolean
* constant TRUE is encoded as the unsigned number 1 accordingly.
*/
#define aiger_false 0
#define aiger_true 1
#define aiger_is_constant(l) \
((l) == aiger_false || ((l) == aiger_true))
#define aiger_sign(l) \
(((unsigned)(l))&1)
#define aiger_strip(l) \
(((unsigned)(l))&~1)
#define aiger_not(l) \
(((unsigned)(l))^1)
/*------------------------------------------------------------------------*/
/* Each literal is associated to a variable having an unsigned index. The
* variable index is obtained by deviding the literal index by two, which is
* the same as removing the sign bit.
*/
#define aiger_var2lit(i) \
(((unsigned)(i)) << 1)
#define aiger_lit2var(l) \
(((unsigned)(l)) >> 1)
/*------------------------------------------------------------------------*/
/* Callback functions for client memory management. The 'free' wrapper will
* get as last argument the size of the memory as it was allocated.
*/
typedef void *(*aiger_malloc) (void *mem_mgr, size_t);
typedef void (*aiger_free) (void *mem_mgr, void *ptr, size_t);
/*------------------------------------------------------------------------*/
/* Callback function for client character stream reading. It returns an
* ASCII character or EOF. Thus is has the same semantics as the standard
* library 'getc'. See 'aiger_read_generic' for more details.
*/
typedef int (*aiger_get) (void *client_state);
/*------------------------------------------------------------------------*/
/* Callback function for client character stream writing. The return value
* is EOF iff writing failed and otherwise the character 'ch' casted to an
* unsigned char. It has therefore the same semantics as 'fputc' and 'putc'
* from the standard library.
*/
typedef int (*aiger_put) (char ch, void *client_state);
/*------------------------------------------------------------------------*/
enum aiger_mode
{
aiger_binary_mode = 0,
aiger_ascii_mode = 1,
aiger_stripped_mode = 2, /* can be ORed with one of the previous */
};
typedef enum aiger_mode aiger_mode;
/*------------------------------------------------------------------------*/
struct aiger_and
{
unsigned lhs; /* as literal [2..2*maxvar], even */
unsigned rhs0; /* as literal [0..2*maxvar+1] */
unsigned rhs1; /* as literal [0..2*maxvar+1] */
};
/*------------------------------------------------------------------------*/
struct aiger_symbol
{
unsigned lit; /* as literal [0..2*maxvar+1] */
unsigned next, reset; /* used only for latches */
unsigned size, * lits; /* used only for justice */
char *name;
};
/*------------------------------------------------------------------------*/
/* This is the externally visible state of the library. The format is
* almost the same as the ASCII file format. The first part is exactly as
* in the header 'M I L O A' and optional 'B C J F' after the format identifier
* string.
*/
struct aiger
{
/* variable not literal index, e.g. maxlit = 2*maxvar + 1
*/
unsigned maxvar;
unsigned num_inputs;
unsigned num_latches;
unsigned num_outputs;
unsigned num_ands;
unsigned num_bad;
unsigned num_constraints;
unsigned num_justice;
unsigned num_fairness;
aiger_symbol *inputs; /* [0..num_inputs[ */
aiger_symbol *latches; /* [0..num_latches[ */
aiger_symbol *outputs; /* [0..num_outputs[ */
aiger_symbol *bad; /* [0..num_bad[ */
aiger_symbol *constraints; /* [0..num_constraints[ */
aiger_symbol *justice; /* [0..num_justice[ */
aiger_symbol *fairness; /* [0..num_fairness[ */
aiger_and *ands; /* [0..num_ands[ */
char **comments; /* zero terminated */
};
/*------------------------------------------------------------------------*/
/* Version and CVS identifier.
*/
const char *aiger_id (void); /* not working after moving to 'git' */
const char *aiger_version (void);
/*------------------------------------------------------------------------*/
/* You need to initialize the library first. This generic initialization
* function uses standard 'malloc' and 'free' from the standard library for
* memory management.
*/
aiger *aiger_init (void);
/*------------------------------------------------------------------------*/
/* Same as previous initialization function except that a memory manager
* from the client is used for memory allocation. See the 'aiger_malloc'
* and 'aiger_free' definitions above.
*/
aiger *aiger_init_mem (void *mem_mgr, aiger_malloc, aiger_free);
/*------------------------------------------------------------------------*/
/* Reset and delete the library.
*/
void aiger_reset (aiger *);
/*------------------------------------------------------------------------*/
/* Treat the literal 'lit' as input, output, latch, bad, constraint,
* justice of fairness respectively. The
* literal of latches and inputs can not be signed nor a constant (< 2).
* You can not register latches nor inputs multiple times. An input can not
* be a latch. The last argument is the symbolic name if non zero.
* The same literal can of course be used for multiple outputs.
*/
void aiger_add_input (aiger *, unsigned lit, const char *);
void aiger_add_latch (aiger *, unsigned lit, unsigned next, const char *);
void aiger_add_output (aiger *, unsigned lit, const char *);
void aiger_add_bad (aiger *, unsigned lit, const char *);
void aiger_add_constraint (aiger *, unsigned lit, const char *);
void aiger_add_justice (aiger *, unsigned size, unsigned *, const char *);
void aiger_add_fairness (aiger *, unsigned lit, const char *);
/*------------------------------------------------------------------------*/
/* Add a reset value to the latch 'lit'. The 'lit' has to be a previously
* added latch and 'reset' is either '0', '1' or equal to 'lit', the latter
* means undefined.
*/
void aiger_add_reset (aiger *, unsigned lit, unsigned reset);
/*------------------------------------------------------------------------*/
/* Register an unsigned AND with AIGER. The arguments are signed literals
* as discussed above, e.g. the least significant bit stores the sign and
* the remaining bit the variable index. The 'lhs' has to be unsigned
* (even). It identifies the AND and can only be registered once. After
* registration an AND can be accessed through 'ands[aiger_lit2idx (lhs)]'.
*/
void aiger_add_and (aiger *, unsigned lhs, unsigned rhs0, unsigned rhs1);
/*------------------------------------------------------------------------*/
/* Add a line of comments. The comment may not contain a new line character.
*/
void aiger_add_comment (aiger *, const char *comment_line);
/*------------------------------------------------------------------------*/
/* This checks the consistency for debugging and testing purposes. In
* particular, it is checked that all 'next' literals of latches, all
* outputs, and all right hand sides of ANDs are defined, where defined
* means that the corresponding literal is a constant 0 or 1, or defined as
* an input, a latch, or AND gate. Furthermore the definitions of ANDs are
* checked to be non cyclic. If a check fails a corresponding error message
* is returned.
*/
const char *aiger_check (aiger *);
/*------------------------------------------------------------------------*/
/* These are the writer functions for AIGER. They return zero on failure.
* The assumptions on 'aiger_put' are the same as with 'fputc' from the
* standard library (see the 'aiger_put' definition above). Note, that
* writing in binary mode triggers 'aig_reencode' and thus destroys the
* original literal association and may even delete AND nodes. See
* 'aiger_reencode' for more details.
*/
int aiger_write_to_file (aiger *, aiger_mode, FILE *);
int aiger_write_to_string (aiger *, aiger_mode, char *str, size_t len);
int aiger_write_generic (aiger *, aiger_mode, void *state, aiger_put);
/*------------------------------------------------------------------------*/
/* The following function allows to write to a file. The write mode is
* determined from the suffix in the file name. The mode used is ASCII for
* a '.aag' suffix and binary mode otherwise. In addition a '.gz' suffix can
* be added which requests the file to written by piping it through 'gzip'.
* This feature assumes that the 'gzip' program is in your path and can be
* executed through 'popen'. The return value is non zero on success.
*/
int aiger_open_and_write_to_file (aiger *, const char *file_name);
/*------------------------------------------------------------------------*/
/* The binary format reencodes all indices. After normalization the input
* indices come first followed by the latch and then the AND indices. In
* addition the indices will be topologically sorted to respect the
* child/parent relation, e.g. child indices will always be smaller than
* their parent indices. This function can directly be called by the
* client. As a side effect, ANDs that are not in any cone of a next state
* function nor in any cone of an output function are discarded. The new
* indices of ANDs start immediately after all input and latch indices. The
* data structures are updated accordingly including 'maxvar'. The client
* data within ANDs is reset to zero.
*/
int aiger_is_reencoded (aiger *);
void aiger_reencode (aiger *);
/*------------------------------------------------------------------------*/
/* This function computes the cone of influence (coi). The coi contains
* those literals that may have an influence to one of the outputs. A
* variable 'v' is in the coi if the array returned as result is non zero at
* position 'v'. All other variables can be considered redundant. The array
* returned is valid until the next call to this function and will be
* deallocated on reset.
*
* TODO: this is just a stub and actually not really implemented yet.
*/
const unsigned char * aiger_coi (aiger *); /* [1..maxvar] */
/*------------------------------------------------------------------------*/
/* Read an AIG from a FILE, a string, or through a generic interface. These
* functions return a non zero error message if an error occurred and
* otherwise 0. The paramater 'aiger_get' has the same return values as
* 'getc', e.g. it returns 'EOF' when done. After an error occurred the
* library becomes invalid. Only 'aiger_reset' or 'aiger_error' can be
* used. The latter returns the previously returned error message.
*/
const char *aiger_read_from_file (aiger *, FILE *);
const char *aiger_read_from_string (aiger *, const char *str);
const char *aiger_read_generic (aiger *, void *state, aiger_get);
/*------------------------------------------------------------------------*/
/* Returns a previously generated error message if the library is in an
* invalid state. After this function returns a non zero error message,
* only 'aiger_reset' can be called (beside 'aiger_error'). The library can
* reach an invalid through a failed read attempt, or if 'aiger_check'
* failed.
*/
const char *aiger_error (aiger *);
/*------------------------------------------------------------------------*/
/* Same semantics as with 'aiger_open_and_write_to_file' for reading.
*/
const char *aiger_open_and_read_from_file (aiger *, const char *);
/*------------------------------------------------------------------------*/
/* Write symbol table or the comments to a file. Result is zero on failure.
*/
int aiger_write_symbols_to_file (aiger *, FILE * file);
int aiger_write_comments_to_file (aiger *, FILE * file);
/*------------------------------------------------------------------------*/
/* Remove symbols and comments. The result is the number of symbols
* and comments removed.
*/
unsigned aiger_strip_symbols_and_comments (aiger *);
/*------------------------------------------------------------------------*/
/* If 'lit' is an input or a latch with a name, the symbolic name is
* returned. Note, that literals can be used for multiple outputs.
* Therefore there is no way to associate a name with a literal itself.
* Names for outputs are stored in the 'outputs' symbols and can only be
* accesed through a linear traversal of the output symbols.
*/
const char *aiger_get_symbol (aiger *, unsigned lit);
/*------------------------------------------------------------------------*/
/* Return tag of the literal:
*
* 0 = constant
* 1 = input
* 2 = latch
* 3 = and
*/
int aiger_lit2tag (aiger *, unsigned lit);
/*------------------------------------------------------------------------*/
/* Check whether the given unsigned, e.g. even, literal was defined as
* 'input', 'latch' or 'and'. The command returns a zero pointer if the
* literal was not defined as 'input', 'latch', or 'and' respectively.
* Otherwise a pointer to the corresponding input or latch symbol is returned.
* In the case of an 'and' the AND node is returned. The returned symbol
* if non zero is in the respective array of 'inputs', 'latches' and 'ands'.
* It thus also allows to extract the position of an input or latch literal.
* For outputs this is not possible, since the same literal may be used for
* several outputs.
*/
aiger_symbol *aiger_is_input (aiger *, unsigned lit);
aiger_symbol *aiger_is_latch (aiger *, unsigned lit);
aiger_and *aiger_is_and (aiger *, unsigned lit);
#endif

426
circuit.cpp Normal file
View File

@ -0,0 +1,426 @@
#include "sweep.hpp"
#include "circuit.hpp"
bool Sweep::match_xor(int x) { // check clause x, -y, -z <==> xor
int y = C[x][0], z = C[x][1];
if (y >= 0 || z >= 0) return false;
if (del[-y] || del[-z] || !C[-y].sz || !C[-z].sz) return false;
int u1 = C[-y][0], v1 = C[-y][1];
int u2 = C[-z][0], v2 = C[-z][1];
if (u1 == -u2 && v1 == -v2) goto doit;
if (u1 == -v2 && v1 == -u2) goto doit;
return false;
doit:
del[x] = 1;
if (C[-y].outs <= 1) del[-y] = 2;
if (C[-z].outs <= 1) del[-z] = 2;
C[x][0] = C[-y][0], C[x][1] = C[-y][1];
C[x].type = Xor;
return true;
}
bool Sweep::match_majority(int x) {
// x = -y & z
// z = -v & -w
// y = a1 & a2
// v = a1 & a3
// w = a2 & a3
int y = C[x][0], z = C[x][1];
if (y > 0) std::swap(y, z);
if (y >= 0 || z <= 0) return false;
if (del[-y] || del[z] || !C[-y].sz || !C[z].sz) return false;
int v = C[z][0], w = C[z][1];
if (v >= 0 || w >= 0) return false;
if (del[-v] || del[-w] || !C[-v].sz || !C[-w].sz) return false;
// -y, -w, -v
int a = C[-y][0], b = C[-y][1];
if (C[-v][1] == a || C[-v][1] == b) std::swap(C[-v][0], C[-v][1]);
if (C[-w][1] == a || C[-w][1] == b) std::swap(C[-w][0], C[-w][1]);
if (C[-v][0] != a && C[-w][0] != a) return false;
if (C[-v][0] != b && C[-w][0] != b) return false;
if (C[-v][1] != C[-w][1]) return false;
del[x] = 1;
if (C[-y].outs <= 1) del[-y] = 2;
if (C[z].outs <= 1) del[z] = 2;
if (C[-v].outs <= 1) del[-v] = 2;
if (C[-w].outs <= 1) del[-w] = 2;
C[x][0] = a; C[x][1] = b;
C[x].push(C[-w][1]);
C[x].type = Majority;
return true;
}
void Sweep::adjust_not() {
int *pos = new int[maxvar + 1];
int *neg = new int[maxvar + 1];
for (int i = 1; i <= maxvar; i++)
pos[i] = neg[i] = 0;
for (int i = 1; i <= maxvar; i++) {
if (!C[i].sz || del[i] == 2) continue;
for (int j = 0; j < C[i].sz; j++) {
int v = C[i][j];
if (v > 0) pos[v]++;
else neg[-v]++;
}
}
for (int i = 1; i <= maxvar; i++) {
if (!C[i].sz || del[i] == 2) continue;
if (C[i].type == Xor && pos[i] == 0 && neg[i] > 0) {
for (int j = 0; j < C[i].sz; j++)
if (C[i][j] < 0 && C[-C[i][j]].neg == 0) {C[i][j] = -C[i][j]; C[i].neg = 1; break;}
}
// if (C[i].type == Xor) {
// int z = 0;
// for (int j = 0; j < C[i].sz; j++)
// if (C[i][j] < 0) {C[i][j] = -C[i][j]; z ^= 1;}
// if (z) C[i].neg = 1;
// }
}
}
void Sweep::match_HA() {
std::map<int, int> M;
int lits = maxvar << 1 | 1;
for (int i = 1; i <= maxvar; i++) {
if (!C[i].sz || del[i] == 2 || C[i].type != And) continue;
int mapid = C[i][0] * lits + C[i][1];
M[mapid] = i;
}
for (int i = 1; i <= maxvar; i++) {
if (!C[i].sz || del[i] == 2 || C[i].type != Xor) continue;
int mapid = C[i][0] * lits + C[i][1];
int id = M[mapid];
if (id) {
C[i].type = HA;
C[i].carrier = id;
del[id] = 2;
continue;
}
mapid = (-C[i][0]) * lits - C[i][1];
id = M[mapid];
if (id) {
C[i].type = HA;
C[i].carrier = id;
C[i][0] = -C[i][0];
C[i][1] = -C[i][1];
del[id] = 2;
continue;
}
mapid = C[i][0] * lits - C[i][1];
id = M[mapid];
if (id) {
C[i].type = HA;
C[i].carrier = id;
C[i][1] = -C[i][1];
C[i].neg = 1;
del[id] = 2;
continue;
}
mapid = (-C[i][0]) * lits + C[i][1];
id = M[mapid];
if (id) {
C[i].type = HA;
C[i].carrier = id;
C[i][0] = -C[i][0];
C[i].neg = 1;
del[id] = 2;
continue;
}
}
}
bool Sweep::line_positive(int to) {
return (to < 0) == C[abs(to)].neg;
}
void Sweep::recalculate_outs() {
for (int i = 1; i <= maxvar; i++)
C[i].outs = 0;
for (int i = 1; i <= maxvar; i++) {
circuit *c = &C[i];
if (!c->sz || del[i] == 2) continue;
for (int j = 0; j < c->sz; j++) {
C[abs(c->to[j])].outs++;
}
}
}
void Sweep::match_FA() {
for (int i = 1; i <= maxvar; i++) {
circuit *c = &C[i];
if (!c->sz || del[i] == 2) continue;
if (c->type != HA) continue;
C[abs(c->carrier)].to.clear();
C[abs(c->carrier)].to.push(i);
C[abs(c->carrier)].sz = 1;
C[abs(c->carrier)].neg = c->carrier < 0;
}
for(int i=1; i<=maxvar; i++) {
if (!C[i].sz || del[i] == 2) continue;
//printf("X: %d\n", i);
circuit *c = &C[i];
if(c->type != And) continue;
if(c->sz != 2) continue;
if(c->to[0] >= 0) continue;
if(c->to[1] >= 0) continue;
if(C[abs(c->to[0])].sz != 1) continue;
if(C[abs(c->to[1])].sz != 1) continue;
int ha1 = C[abs(c->to[0])][0];
int ha2 = C[abs(c->to[1])][0];
ha1 = abs(ha1);
ha2 = abs(ha2);
if(C[ha1].type != HA) continue;
if(C[ha2].type != HA) continue;
bool check_link = true;
for(int k=0; k<C[ha1].sz; k++) {
int t = C[ha1].to[k];
if(abs(t) == ha2) std::swap(ha1, ha2);
if(abs(t) == ha2 && !line_positive(t))
check_link = false;
}
for(int k=0; k<C[ha2].sz; k++) {
int t = C[ha2].to[k];
if(abs(t) == ha1 && !line_positive(t))
check_link = false;
}
if(!check_link) continue;
//printf("FA %d(%d) %d(%d)\n", ha1, C[ha1].neg, ha2, C[ha2].neg);
if(C[ha1].outs == 2) del[ha1] = 2;
circuit* fa = &C[ha2];
fa->type = FA;
fa->carrier = -i;
vec<int> new_vec;
for(int k=0; k<C[ha1].sz; k++) {
int t = C[ha1].to[k];
if(abs(t) == ha2) continue;
new_vec.push(t);
//printf("push: %d\n", t);
}
for(int k=0; k<C[ha2].sz; k++) {
int t = C[ha2].to[k];
if(abs(t) == ha1) continue;
//printf("push: %d\n", k, t);
new_vec.push(t);
}
new_vec.copyTo(fa->to);
fa->sz = fa->to.size();
C[i].to.clear();
C[i].sz = 0;
C[i].neg = !C[i].neg;
}
}
void Sweep::to_multi_input_gates() {
//printf("hello\n %d\n", maxvar);
std::queue<int> q;
q.push(maxvar);
while(!q.empty()) {
int u = q.front();
q.pop();
circuit *c = &C[u];
if(u == maxvar) {
for(int i=0; i<c->sz; i++) {
if (!C[abs(c->to[i])].sz || del[abs(c->to[i])] == 2) continue;
q.push(abs(c->to[i]));
}
continue;
}
for(int i=0; i<c->sz; i++) {
circuit *t = &C[abs(c->to[i])];
if(t->type != c->type) continue;
vec<int> new_vec;
if(c->type == Xor) {
//printf("XOR: %d %d\n", u, c->to[i]);
for(int j=0; j<t->sz; j++) {
new_vec.push(t->to[j]);
//printf("add %d\n", t->to[j]);
}
for(int j=0; j<c->sz; j++) {
if(i == j) {
if(!line_positive(c->to[j]))
new_vec[0] = -new_vec[0];
} else {
new_vec.push(c->to[j]);
}
}
if(t->outs == 1) {
del[abs(c->to[i])] = 2;
//printf("del: %d\n", c->to[i]);
}
new_vec.copyTo(c->to);
c->sz = new_vec.size();
q.push(u);
break;
}
if(c->type == And && line_positive(c->to[i])) {
if(t->to.size() == 0) continue;
//printf("AND: %d %d\n", u, c->to[i]);
t->to.copyTo(new_vec);
//printf("new_vec %d\n", new_vec.size());
for(int j=0; j<c->sz; j++) {
if(i != j) {
new_vec.push(c->to[j]);
}
}
if(C[abs(c->to[i])].outs == 1) {
del[abs(c->to[i])] = 2;
}
new_vec.copyTo(c->to);
c->sz = new_vec.size();
q.push(u);
break;
}
}
for(int i=0; i<c->sz; i++) {
if (!C[abs(c->to[i])].sz || del[abs(c->to[i])] == 2) continue;
q.push(abs(c->to[i]));
}
}
}
void Sweep::to_dot_graph(const char* filename, int end_point) {
std::ofstream file(filename);
std::queue<int> q;
q.push(abs(end_point));
std::set<int> used;
used.insert(abs(end_point));
file << "digraph \"graph\" {\n";
char str[1024];
while(!q.empty()) {
int u = q.front();
q.pop();
circuit *c = &C[u];
if(!c->sz || del[u] == 2) continue;
sprintf(str, "A%d[label=\"%d (%s)\"];\n", u, u, gate_type[c->type].c_str());
file << str;
if (c->type == HA || c->type == FA) {
int a = u * (C[u].neg ? -1 : 1);
int b = c->carrier;
sprintf(str, "A%d->A%d[arrowhead=%s]\n", u, abs(b), !line_positive(b) ? "dot" : "none");
file << str;
}
else {
int t = u * (C[u].neg ? -1 : 1);
}
for (int j = 0; j < c->sz; j++) {
/**
* 删除初始输入
*/
if(abs(c->to[j]) <= num_inputs) continue;
sprintf(str, "A%d->A%d[arrowhead=%s]\n", abs(c->to[j]), u, !line_positive(c->to[j]) ? "dot" : "none");
file << str;
}
for(int j=0; j<c->sz; j++) {
int x = abs(c->to[j]);
if(used.count(x)) continue;
used.insert(x);
q.push(x);
}
}
file << "}\n";
}
void Sweep::identify() {
del = new int[maxvar + 1];
for (int i = 1; i <= maxvar; i++) del[i] = 0;
recalculate_outs();
for (int i = 1; i <= maxvar; i++) {
if (!C[i].sz || del[i] == 2) continue;
if (match_xor(i)) continue;
}
recalculate_outs();
for (int i = 1; i <= maxvar; i++) {
if (!C[i].sz || del[i] == 2) continue;
if (match_majority(i)) continue;
}
recalculate_outs();
adjust_not();
match_HA();
to_multi_input_gates();
match_FA();
// printf("digraph \"graph\" {\n");
// for (int i = 1; i <= maxvar; i++) {
// circuit *c = &C[i];
// if (!c->sz || del[i] == 2) continue;
// printf("A%d[label=\"%d (%s)\"];\n", i, i, gate_type[c->type].c_str());
// if (c->type == HA || c->type == FA) {
// int a = i * (C[i].neg ? -1 : 1);
// int b = c->carrier;
// printf("A%d->A%d[arrowhead=%s]\n", i, abs(b), !line_positive(b) ? "dot" : "none");
// }
// else {
// int t = i * (C[i].neg ? -1 : 1);
// }
// for (int j = 0; j < c->sz; j++) {
// if(abs(c->to[j]) <= 14) continue;
// printf("A%d->A%d[arrowhead=%s]\n", abs(c->to[j]), i, !line_positive(c->to[j]) ? "dot" : "none");
// }
// }
// printf("}\n");
//to_dot_graph("graph1.dot", abs(C[maxvar].to[0]));
//to_dot_graph("graph2.dot", abs(C[maxvar].to[1]));
// recalculate_outs();
// for (int i = 1; i <= maxvar; i++) {
// circuit *c = &C[i];
// if (del[i] == 2) continue;
// printf("%d : %d (outs)\n", i, c->outs);
// }
}

16
circuit.hpp Normal file
View File

@ -0,0 +1,16 @@
#ifndef circuit_hpp_INCLUDED
#define circuit_hpp_INCLUDED
enum gate_type {And, Xor, Majority, HA, FA};
const std::string gate_type[5] = {"and", "xor", "majority", "HA", "FA"};
struct circuit {
vec<int> to;
int sz, outs, type, neg, carrier;
circuit() : sz(0), outs(0), type(0), neg(0), carrier(0) {}
void push(int x) { to.push(x); sz++; }
int &operator [] (int index) { return to[index]; }
const int& operator [] (int index) const { return to[index]; }
};
#endif

1
f4cpp Submodule

@ -0,0 +1 @@
Subproject commit 645458ca02450215bd0e891fc3081d8cbc79c51f

BIN
lib/libopenf4.so.0 Executable file
View File

Binary file not shown.

BIN
lib/libopenf4.so.0.0.0 Executable file
View File

Binary file not shown.

1
m4gb Submodule

@ -0,0 +1 @@
Subproject commit 0a166c87ab7d156ccbbff807a0ad1ec50cff8d83

38
makefile Normal file
View File

@ -0,0 +1,38 @@
SRCS = $(shell find . -maxdepth 1 -name "*.c*")
BUILD_DIR = build/
OBJS = $(addprefix $(BUILD_DIR), $(addsuffix .o, $(basename $(SRCS))))
EXEC = acec
LIBS = -lgmp -Iopenf4 -Llib -lopenf4
CXXFLAGS=-O3 -std=c++17
$(EXEC): $(OBJS)
$(CXX) -o $@ $^ $(CXXFLAGS) $(LIBS)
$(BUILD_DIR)%.o: %.cpp
$(CXX) -c $< -o $@ $(CXXFLAGS) $(LIBS)
$(BUILD_DIR)%.o: %.c
gcc -c $< -o $@ $(CXXFLAGS) $(LIBS)
clean:
rm -f $(OBJS) $(EXEC)
# CFLAGS=-O3
# solver: aiger.o main.o $(LIBS)
# $(CXX) $^ -o $@
# aiger.o: aiger.c aiger.h
# $(C) $(CFLAGS) -c $< -o $@
# main.o: main.cpp aiger.h
# $(CC) $(CXXFLAGS) -c $< -o $@
# clean:
# rm -rf *.o
# rm -rf solver

1
mathic Submodule

@ -0,0 +1 @@
Subproject commit 66b5d74f8417459414cbf3753cfa9a0128483cbd

1
openf4 Submodule

@ -0,0 +1 @@
Subproject commit 7155c6ec4e5f776e0e12202716dc7da58469e77b

0
result.txt Normal file
View File

76
sweep.cpp Normal file
View File

@ -0,0 +1,76 @@
#include "sweep.hpp"
#include "circuit.hpp"
extern "C" {
#include "aiger.h"
}
int Sweep::get_time() {
return std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - clk_st).count();
}
void Sweep::aiger_preprocess() {
aiger_read_from_file(aig, file);
maxvar = aig->maxvar;
output = aig->outputs[0].lit;
num_inputs = aig->num_inputs;
used = new int[maxvar + 1];
C = new circuit[maxvar + 1];
memset(used, 0, (maxvar + 1) * sizeof(int));
sum_pos = new int[2 * maxvar + 2];
sum_neg = new int[2 * maxvar + 2];
memset(sum_pos, 0, sizeof(int) * (2 * maxvar + 2));
memset(sum_neg, 0, sizeof(int) * (2 * maxvar + 2));
for(int i=0; i<aig->num_ands; i++) {
auto gate = aig->ands[i];
int o = aiger_lit2var(gate.lhs);
int i0 = aiger_lit2var(gate.rhs0);
int i1 = aiger_lit2var(gate.rhs1);
graph.add(i0, o, gate.rhs0 & 1);
graph.add(i1, o, gate.rhs1 & 1);
assert((gate.lhs & 1) == 0);
C[o].push(i0 * (gate.rhs0 & 1 ? -1 : 1));
C[o].push(i1 * (gate.rhs1 & 1 ? -1 : 1));
}
// for (int i = 1; i <= maxvar; i++) {
// circuit *c = &C[i];
// if (!c->sz) continue;
// printf("%d = %s ( ", i, gate_type[c->type].c_str());
// for (int j = 0; j < c->sz; j++) {
// printf("%d ", c->to[j]);
// }
// puts(")");
// }
return;
printf("c inputs: \nc ");
for(int i=0; i<aig->num_inputs; i++) {
printf("%d ", aig->inputs[i].lit);
}
printf("\nc outputs: \nc ");
for(int i=0; i<aig->num_outputs; i++) {
printf("%d ", aig->outputs[i].lit);
}
printf("\nc maxvar: \nc %d\n", maxvar);
// int x = det_v > 0 ? det_v : -det_v;
// if (x > maxvar) det_v = 0;
printf("assume:");
for (int i = 0; i < det_v_sz; i++) {
printf(" %d", det_v[i]);
}
puts("");
cal_topo_index();
}
void Sweep::solve() {
aiger_preprocess();
printf("c preprocess finish: %.2lf s\n", 0.001 * get_time());
identify();
printf("c identify finish: %.2lf s\n", 0.001 * get_time());
}

100
sweep.hpp Normal file
View File

@ -0,0 +1,100 @@
#ifndef sweep_hpp_INCLUDED
#define sweep_hpp_INCLUDED
#include <chrono>
#include <bits/stdc++.h>
#include <cstring>
#include "vec.hpp"
namespace CaDiCaL {
struct Solver;
}
struct aiger;
struct circuit;
class Graph {
public:
struct Edge {
int from;
int to;
int neg;
};
std::vector<std::vector<Edge>> edge;
std::vector<std::vector<Edge>> redge;
void add(int u, int v, int w) {
edge.resize(std::max(std::max(u, v)+1, (int)edge.size()));
redge.resize(std::max(std::max(u, v)+1, (int)redge.size()));
edge[u].push_back(Edge{u, v, w});
redge[v].push_back(Edge{v, u, w});
}
};
class Sweep {
public:
FILE* file;
Graph graph;
int maxvar, output, num_inputs;
int *used, *det_v, *is_cut, *sum_pos, *sum_neg, *del;
int det_v_sz = 0;
int rounds;
std::chrono::high_resolution_clock::time_point clk_st = std::chrono::high_resolution_clock::now();
circuit *C;
aiger *aig;
std::map<int, int> topo_index;
void solve();
void aiger_preprocess();
void cal_topo_index();
void propagate(int* input, int* result);
void random_simulation();
void simulation();
bool check_var_equal(int x, int y, int assume);
bool check_constant(int x, int val);
void check_entire_problem(aiger* aig);
void check_with_SAT();
void identify();
bool match_xor(int x);
bool match_majority(int x);
void adjust_not();
void match_HA();
void match_FA();
bool line_positive(int to);
void recalculate_outs();
void to_multi_input_gates();
void simplify();
void miter();
void to_dot_graph(const char* filename, int end_point);
int get_time();
};
#endif

95
vec.hpp Normal file
View File

@ -0,0 +1,95 @@
#ifndef _vec_hpp_INCLUDED
#define _vec_hpp_INCLUDED
#include <cassert>
#include <cstdio>
#include <cstdlib>
#include <cerrno>
#include <cstddef>
#include <cstring>
#include <fstream>
template<class T>
class vec {
static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
static inline void nextCap(int &cap) { cap += ((cap >> 1) + 2) & ~1; }
public:
T* data;
int sz, cap;
vec() : data(NULL), sz(0), cap(0) {}
vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
explicit vec(int size) : data(NULL), sz(0), cap(0) { growTo(size); }
~vec() { clear(true); }
operator T* (void) { return data; }
int size (void) const { return sz; }
int capacity (void) const { return cap; }
void capacity (int min_cap);
void setsize (int v) { sz = v;}
void push (void) { if (sz == cap) capacity(sz + 1); new (&data[sz]) T(); sz++; }
void push (const T& elem) { if (sz == cap) capInc(sz + 1); data[sz++] = elem; }
void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
void pop (void) { assert(sz > 0), sz--, data[sz].~T(); }
void copyTo (vec<T>& copy) { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
void growTo (int size);
void growTo (int size, const T& pad);
void clear (bool dealloc = false);
void capInc (int to_cap);
T& operator [] (int index) { return data[index]; }
const T& operator [] (int index) const { return data[index]; }
T& last (void) { return data[sz - 1]; }
const T& last (void) const { return data[sz - 1]; }
};
class OutOfMemoryException{};
template<class T>
void vec<T>::clear(bool dealloc) {
if (data != NULL) {
sz = 0;
if (dealloc) free(data), data = NULL, cap = 0;
}
}
template<class T>
void vec<T>::capInc(int to_cap) {
if (cap >= to_cap) return;
int add = imax((to_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);
if (add > __INT_MAX__ - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
throw OutOfMemoryException();
}
template<class T>
void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
if (add > __INT_MAX__ - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
throw OutOfMemoryException();
}
template<class T>
void vec<T>::growTo(int size) {
if (sz >= size) return;
capInc(size);
for (int i = 0; i < sz; i++) new (&data[i]) T();
sz = size;
}
template<class T>
void vec<T>::growTo(int size, const T& pad) {
if (sz >= size) return;
capacity(size);
for (int i = sz; i < size; i++) data[i] = pad;
sz = size; }
#endif

1
z3 Submodule

@ -0,0 +1 @@
Subproject commit e2cfc53c9fe44690bf4310ad0ce8d0b6deea91f5